Commit bfb48dbb authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen

merged with master

parents fb3145be d2147936
Pipeline #10171 failed with stage
in 0 seconds
*.vo
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
......
......@@ -2,24 +2,17 @@ image: ralfjung/opam-ci:latest
stages:
- build
- deploy
- build_more
variables:
CPU_CORES: "9"
CPU_CORES: "10"
GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template
stage: build
tags:
- fp-timing
- fp
script:
# prepare
- . build/opam-ci.sh $OPAM_PINS
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
......@@ -27,51 +20,48 @@ variables:
only:
- master
- /^ci/
opam:
stage: deploy
script:
# Send a trigger to the repository doing the work
- curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline
variables:
OPAM_PKG: "coq-iris"
only:
- master
except:
- triggers
- schedules
reverse-deps:
stage: deploy
script:
# Send a trigger to reverse dependencies to have them tested
- curl --fail -X POST -F "token=$IRIS_EXAMPLES_SECRET" -F "ref=master" -F "variables[IRIS_REV]=$CI_COMMIT_SHA" https://gitlab.mpi-sws.org/api/v4/projects/615/trigger/pipeline
only:
- master
except:
- triggers
## Build jobs
build-coq.8.7.dev:
build-coq.dev:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
except:
- triggers
OPAM_PINS: "coq version dev"
VALIDATE: "1"
build-coq.8.8.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
OPAM_PKG: "coq-iris"
TIMING_PROJECT: "iris"
TIMING_CONF: "coq-8.7.2"
tags:
- fp-timing
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
build-coq.8.7.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.0 coq-mathcomp-ssreflect version 1.6.4"
except:
- triggers
OPAM_PINS: "coq version 8.7.0"
build-coq.8.6.1:
build-stdpp.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
artifacts:
paths:
- build-time.txt
- build-env.txt
OPAM_PINS: "coq version 8.7.2 coq-stdpp.dev git https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/#$STDPP_REV"
except:
only:
- triggers
- schedules
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
......@@ -3,7 +3,33 @@ way the logic is used on paper. We also mention some significant changes in the
Coq development, but not every API-breaking change is listed. Changes marked
`[#]` still need to be ported to the Iris Documentation LaTeX file(s).
## Iris 3.1.0 (unfinished)
## Iris master
Changes in and extensions of the theory:
* [#] Add weakest preconditions for total program correctness.
* [#] "(Potentially) stuck" weakest preconditions are no longer considered
experimental.
Changes in Coq:
* Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
* The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead of
in `Prop` using `exists`. This makes it possible to define the function space
CMRA even for an infinite domain.
* Rename proof mode type classes for laters:
- `IntoLaterN``MaybeIntoLaterN` (this one _may_ strip a later)
- `IntoLaterN'``IntoLaterN` (this one _should_ strip a later)
- `IntoLaterNEnv``MaybeIntoLaterNEnv`
- `IntoLaterNEnvs``MaybeIntoLaterNEnvs`
* Rename:
- `frag_auth_op``frac_auth_frag_op`
- `cmra_opM_assoc``cmra_op_opM_assoc`
- `cmra_opM_assoc_L``cmra_op_opM_assoc_L`
- `cmra_opM_assoc'``cmra_opM_opM_assoc`
* `namespaces` has been moved to std++.
## Iris 3.1.0 (released 2017-12-19)
Changes in and extensions of the theory:
......
# CONTRIBUTING TO THE IRIS COQ DEVELOPMENT
# Contributing to the Iris Coq Development
Discussion about the Iris Coq development happens on the mailing list
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club).
This is also the right place to ask questions.
If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues). You will have
to create an account at the
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club) and
in the [Iris Chat](https://mattermost.mpi-sws.org/iris). This is also the right
place to ask questions. The chat requires an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab).
To contribute code, please send your MPI-SWS GitLab username to
[Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
your account. Then you can fork the
If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
requires an MPI-SWS GitLab account. To contribute code, please send your
MPI-SWS GitLab username to [Ralf Jung](https://gitlab.mpi-sws.org/jung) to
enable personal projects for your account. Then you can fork the
[Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
changes in your fork, and create a merge request.
Here we collect some information on how to set up your editor to properly input
and output the unicode characters used throughout Iris.
## General: Unicode Fonts
Most editors will just use system fonts for rendering unicode characters and do
not need furhter configuration once the fonts are installed. Here are some
combinations of fonts that are known to give readable results (i.e., each of
these sets of fonts covers all the required characters):
* Fira Mono, DejaVu Mono, Symbola
## Emacs
### Unicode Input
First, install `math-symbol-lists` by doing `M-x package-install math-symbol-lists`.
Next, add the following to your `~/.emacs` to configure an input method based on the math symbol list, and with some custom aliases for symbols used a lot in Iris:
```
;; Input of unicode symbols
(require 'math-symbol-lists)
; Automatically use math input method for Coq files
(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
; Input method for the minibuffer
(defun my-inherit-input-method ()
"Inherit input method from `minibuffer-selected-window'."
(let* ((win (minibuffer-selected-window))
(buf (and win (window-buffer win))))
(when buf
(activate-input-method (buffer-local-value 'current-input-method buf)))))
(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
; Define the actual input method
(quail-define-package "math" "UTF-8" "Ω" t)
(quail-define-rules ; add whatever extra rules you want to define here...
("\\mult" ?⋅)
("\\ent" ?⊢)
("\\valid" ?✓)
("\\box" ?□)
("\\later" ?▷)
("\\pred" ?φ)
("\\and" ?∧)
("\\or" ?∨)
("\\comp" ?∘)
("\\ccomp" ?◎)
("\\all" ?∀)
("\\ex" ?∃)
("\\to" ?→)
("\\sep" ?∗)
("\\lc" ?⌜)
("\\rc" ?⌝)
("\\lam" ?λ)
("\\empty" ?∅)
("\\Lam" ?Λ)
("\\Sig" ?Σ)
("\\-" ?∖)
("\\aa" ?●)
("\\af" ?◯)
("\\iff" ?↔)
("\\gname" ?γ)
("\\incl" ?≼)
("\\latert" ?▶)
)
(mapc (lambda (x)
(if (cddr x)
(quail-defrule (cadr x) (car (cddr x)))))
(append math-symbol-list-basic math-symbol-list-extended))
```
### Font Configuration
Even when usable fonts are installed, Emacs tends to pick bad fonts for some
symbols like universal and existential quantifiers. The following configuration
results in a decent choice for the symbols used in Iris:
```
;; Fonts
(set-face-attribute 'default nil :height 110) ; height is in 1/10pt
(dolist (ft (fontset-list))
; Main font
(set-fontset-font ft 'unicode (font-spec :name "Monospace"))
; Fallback font
; Appending to the 'unicode list makes emacs unbearably slow.
;(set-fontset-font ft 'unicode (font-spec :name "DejaVu Sans Mono") nil 'append)
(set-fontset-font ft nil (font-spec :name "DejaVu Sans Mono"))
)
; Fallback-fallback font
; If we 'append this to all fontsets, it picks Symbola even for some cases where DejaVu could
; be used. Adding it only to the "t" table makes it Do The Right Thing (TM).
(set-fontset-font t nil (font-spec :name "Symbola"))
```
......@@ -8,19 +8,19 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories $$(test -d tests && echo tests) \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
build-dep/opam: opam Makefile
# Creating the build-dep package.
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
......@@ -31,12 +31,15 @@ build-dep: build-dep/opam phony
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything.
@# Upgrading is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
((! opam --version | grep "^1\." > /dev/null) || ( \
echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
uninstall::
@# This makes sure we also delete stale files in the destination directory
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
# Naming conventions for variables/arguments/hypotheses in the Coq development
## small letters
* a : A = cmraT or cofeT
* b : B = cmraT or cofeT
* c
* d
* e : expr = expressions
* f = some generic function
* g = some generic function
* h : heap
* i
* j
* k
* l
* m : iGst = ghost state
* n
* o
* p
* q
* r : iRes = resources
* s = state (STSs)
* s = stuckness bits
* t
* u
* v : val = values of language
* w
* x
* y
* z
## capital letters
* A : Type, cmraT or cofeT
* B : Type, cmraT or cofeT
* C
* D
* E : coPset = Viewshift masks
* F = a functor
* G
* H = hypotheses
* I = indexing sets
* J
* K : ectx = evaluation contexts
* K = keys of a map
* L
* M = maps / global CMRA
* N : namespace
* O
* P : uPred, iProp or Prop
* Q : uPred, iProp or Prop
* R : uPred, iProp or Prop
* S : set state = state sets in STSs
* T : set token = token sets in STSs
* U
* V : abstraction of value type in frame shift assertions
* W
* X : sets
* Y : sets
* Z : sets
## small greek letters
* γ : gname
* σ : state = state of language
* φ : interpretation of STS/Auth
## capital greek letters
* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over uPred, iProp or Prop)
# Naming conventions for algebraic classes in the Coq development
## Suffixes
* C: OFEs
* R: cameras
* UR: unital cameras or resources algebras
* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
* G: global camera functor management
* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
......@@ -41,8 +41,8 @@ Context management
the resulting goal.
- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
eliminates it. This tactic is essentially the same as `iDestruct` with the
difference that when `pm_trm` is a non-univerisally quantified spatial
hypothesis, it will not throw the hypothesis away.
difference that when `pm_trm` is a non-univerisally quantified persistent
hypothesis, it will not throw away the hypothesis.
- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
hypothesis `P` to the current goal. The specialization pattern `spat`
specifies which hypotheses will be consumed by proving `P`. The introduction
......@@ -150,11 +150,22 @@ Induction
variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
and the spatial context.
Rewriting
---------
Rewriting / simplification
--------------------------
- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
equality in the proof mode goal / hypothesis `H`.
- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
with the resulting `P`, which in turn becomes the new proof mode goal /
hypothesis `H`.
Note that parentheses around `tac` are needed.
- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
hypothesis `H`. This is a shorthand for `iEval (simpl)`.
- `iRewrite pm_trm` : rewrite an equality in the conclusion.
- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
Iris
----
......
......@@ -6,33 +6,45 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
This version is known to compile with:
- Coq 8.6.1 / 8.7.0
- Ssreflect 1.6.4
- Coq 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0
- A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
For a version compatible with Coq 8.6, have a look at the
[iris-3.1 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.1).
If you need to work with Coq 8.5, please check out the
[iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
The easiest way to install the correct versions of the dependencies is through
opam. You will need the Coq and Iris opam repositories:
## Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add
the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released
Then you can do `opam install coq-iris`.
To obtain a development version, add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## Building from source
## Updating
When building Iris from source, we recommend to use opam (1.2.2 or newer) for
installing Iris's dependencies. This requires the following two repositories:
After doing `git pull`, the development may fail to compile because of outdated
dependencies. To fix that, please run `opam update` followed by
`make build-dep`.
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
## Building
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
To update Iris, do `git pull`. After an update, the development may fail to
compile because of outdated dependencies. To fix that, please run `opam update`
followed by `make build-dep`.
## Directory Structure
* The folder [algebra](theories/algebra) contains the COFE and CMRA
......@@ -62,11 +74,15 @@ CPU cores.
infrastructure. Users of the Iris Coq library should *not* depend on these
modules; they may change or disappear without any notice.
## Documentation
## Further Documentation
A LaTeX version of the core logic definitions and some derived forms is
available in [docs/iris.tex](docs/iris.tex). A compiled PDF version of this
document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
* A LaTeX version of the core logic definitions and some derived forms is
available in [docs/iris.tex](docs/iris.tex). A compiled PDF version of this
document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md).
* Naming conventions are documented at [Naming.md](Naming.md).
## Case Studies
......
......@@ -22,6 +22,7 @@ theories/algebra/vector.v
theories/algebra/updates.v
theories/algebra/local_updates.v
theories/algebra/gset.v
theories/algebra/gmultiset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/base_logic/upred.v
......@@ -38,7 +39,6 @@ theories/base_logic/fixpoint.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/namespaces.v
theories/base_logic/lib/wsat.v
theories/base_logic/lib/invariants.v
theories/base_logic/lib/fancy_updates.v
......@@ -58,12 +58,16 @@ theories/base_logic/lib/fancy_updates_from_vs.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
theories/program_logic/total_weakestpre.v
theories/program_logic/total_adequacy.v
theories/program_logic/hoare.v
theories/program_logic/language.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
......@@ -77,19 +81,7 @@ theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/counter.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/dist_lang/lang.v
theories/dist_lang/tactics.v
theories/dist_lang/lifting.v
theories/dist_lang/notation.v
theories/dist_lang/lib/spawn.v
theories/dist_lang/lib/par.v
theories/dist_lang/lib/assert.v
theories/dist_lang/lib/lock.v
theories/dist_lang/lib/spin_lock.v
theories/dist_lang/lib/ticket_lock.v
theories/dist_lang/lib/counter.v
theories/dist_lang/proofmode.v
theories/dist_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
......@@ -19,17 +19,5 @@
next
}
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines
1
__pycache__
build-times.log*
build-times*
gitlab-extract
......@@ -3,8 +3,6 @@ import argparse, sys, pprint, itertools, subprocess
import requests
import parse_log
markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
# read command-line arguments
parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana')
parser.add_argument("-f", "--file",
......@@ -19,6 +17,9 @@ parser.add_argument("-p", "--project",
parser.add_argument("-b", "--branch",
dest="branch", required=True,
help="Branch name sent to the server.")
parser.add_argument("--config",
dest="config", required=True,
help="The config string.")
parser.add_argument("-s", "--server",
dest="server", required=True,
help="The server (URL) to send the data to.")
......@@ -39,10 +40,11 @@ if args.commits:
results = list(results)
for datapoint in results:
times = ''.join(datapoint.times)
times = '\n'.join(datapoint.times)
commit = datapoint.commit
print("Sending {}...".format(commit), end='')
date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8')
headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Date': date}
r = requests.post(args.server, data=times, headers=headers, auth=(args.user, args.password))
headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
r = requests.post(args.server+"/build_times", data=times, headers=headers, auth=(args.user, args.password))
print(" {}".format(r.text.strip()))
r.raise_for_status()
#!/usr/bin/env python3
import argparse, pprint, sys, glob, zipfile
import argparse, pprint, sys, glob, zipfile, subprocess
import requests
import parse_log
......@@ -40,6 +40,9 @@ parser.add_argument("-c", "--commits",
parser.add_argument("-a", "--artifacts",
dest="artifacts",
help="Location of the artifacts (following GitLab's folder structure). If not given (which should be the common case), the artifacts will be downloaded from GitLab.")
parser.add_argument("-b", "--blacklist-branch",
dest="blacklist_branch",
help="Skip the commit if it is contained in the given branch.")
args = parser.parse_args()
log_file = sys.stdout if args.file == "-" else open(args.file, "a")
......@@ -60,7 +63,13 @@ BREAK = False
for commit in parse_log.parse_git_commits(args.commits):
if BREAK:
break
print("Fetching {}...".format(commit))
# test to skip the commit
if args.blacklist_branch is not None:
branches = subprocess.check_output(["git", "branch", "-r", "--contains", commit]).decode("utf-8")
if args.blacklist_branch in map(lambda x: x.strip(), branches.split('\n')):
continue
# Find out more about the commit
print("Fetching {}...".format(commit), end='')
commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
if commit_data.status_code != 200:
raise Exception("Commit not found?")
......@@ -68,10 +77,12 @@ for commit in parse_log.parse_git_commits(args.commits):
if builds.status_code != 200:
raise Exception("Build not found?")
# iterate over builds by decreasing ID, and look for the artifact
found_build = False
for build in builds.json():
if build['status'] in ('created', 'pending', 'running'):
# build still not yet done, don't fetch this or any later commit
BREAK = True
print(" build still in progress, aborting")
break
if build['status'] != 'success':
# build failed or cancelled, skip to next
......@@ -100,4 +111,8 @@ for commit in parse_log.parse_git_commits(args.commits):
log_file.write(build_times.text)
log_file.flush()
# don't fetch another build
found_build = True
print(" success")
break
if not found_build and not BREAK:
print(" found no succeessful build")
......@@ -17,6 +17,7 @@ def parse(file, parse_times = PARSE_FULL):
commit = None
times = None
for line in file:
line = line.strip()
# next commit?
m = commit_re.match(line)
if m is not None:
......@@ -40,6 +41,7 @@ def parse(file, parse_times = PARSE_FULL):
times[name] = time
continue
# nothing else we know about, ignore
print("Ignoring line",line,"(in commit {})".format(commit))
# end of file. previous commit, if any, is done now.
if commit is not None:
yield Result(commit, times)
......
#!/bin/bash
set -e
set -x
## This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM.
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
eval `opam conf env`
# Make sure the pin for the builddep package is not stale.