diff options
| -rw-r--r-- | .gitlab-ci.yml | 46 | ||||
| -rw-r--r-- | INSTALL.md | 26 | ||||
| -rw-r--r-- | coq-mathcomp-ssreflect.opam | 2 |
3 files changed, 62 insertions, 12 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b8c9c8f..aa05051 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -4,7 +4,7 @@ # (Dockerfile containing: "opam switch set $compiler && eval $(opam env)") # - master (protected branch) => push on GitLab registry and Docker Hub # - other branches (not tags) => push on GitLab registry -# - Todo: GitHub PRs => push on GitLab +# - GitHub PRs => push on GitLab and report back thanks to @coqbot # - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6) # - script template foreach project (custom CONTRIB_URL, script) # - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION) @@ -67,6 +67,9 @@ coq-8.7: coq-8.8: extends: .opam-build +coq-8.9: + extends: .opam-build + coq-dev: extends: .opam-build @@ -117,6 +120,7 @@ make-coq-latest: # - Add 1 job per Coq version to test, that extends the previous hidden job, # and sets vars COQ_VERSION, CONTRIB_VERSION (compatible Git branch/tag) +# The Four Color Theorem .ci-fourcolor: extends: .ci variables: @@ -146,3 +150,43 @@ ci-fourcolor-dev: extends: .ci-fourcolor variables: COQ_VERSION: "dev" + +# The Odd Order Theorem +.ci-odd-order: + extends: .ci + variables: + CONTRIB_URL: "https://github.com/math-comp/odd-order.git" + CONTRIB_VERSION: master + script: + - make -j "${NJOBS}" + - make install + +ci-odd-order-8.7: + extends: .ci-odd-order + variables: + COQ_VERSION: "8.7" + +# The Lemma Overloading library +.ci-lemma-overloading: + extends: .ci + variables: + CONTRIB_URL: "https://github.com/coq-community/lemma-overloading.git" + CONTRIB_VERSION: master + script: + - opam pin add -n -k path coq-lemma-overloading . + - opam install -y -v -j "${NJOBS}" coq-lemma-overloading + +ci-lemma-overloading-8.8: + extends: .ci-lemma-overloading + variables: + COQ_VERSION: "8.8" + +ci-lemma-overloading-8.9: + extends: .ci-lemma-overloading + variables: + COQ_VERSION: "8.9" + +ci-lemma-overloading-dev: + extends: .ci-lemma-overloading + variables: + COQ_VERSION: "dev" @@ -12,7 +12,7 @@ If you just installed OPAM you may have to do the following. You may also want to read [OPAM user manual](https://opam.ocaml.org/doc/Usage.html) first. ``` opam init -eval `opam config env` +eval $(opam config env) ``` Once your OPAM environment is configured you can install any math-comp package via @@ -38,7 +38,7 @@ If you want to install the library in a dedicated environment current OPAM setup you can run the following commands: ``` opam init --root=$PWD/MC -eval `opam config env --root=$PWD/MC` +eval $(opam config env --root=$PWD/MC`) ``` After that the installations instructions above apply. @@ -73,22 +73,28 @@ To install the compiled library, just execute `make install`. ## Compilation and installation of a custom version using OPAM -The instructions assume you are in the `mathcomp` directory -and that you have OPAM installed and configured with the -standard Coq repositories. +The instructions assume you are in the parent directory (that contains +this file `INSTALL.md`) and that you have OPAM installed and +configured with the standard Coq repositories. -For each package, pin the `opam` file: +First, we recommend pinning a particular version of Coq +(here `8.8.0`): ``` -opam pin -n add ssreflect +opam pin add -n coq -k version 8.8.0 +``` + +Then for each math-comp package, pin the `opam` file: ``` +opam pin add -n -k path coq-mathcomp-ssreflect . +``` + This can be achieved in one go as follows: ``` -for P in */opam; do opam pin -n add ${P%%/opam}; done +for P in *.opam; do opam pin add -n -k path ${P%.opam} .; done ``` Then you can use `opam install` to compile and install any package. For example: ``` -opam install coq.8.8.0 coq-mathcomp-ssreflect +opam install coq-mathcomp-character -j3 ``` - diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam index 5d31846..a018a3e 100644 --- a/coq-mathcomp-ssreflect.opam +++ b/coq-mathcomp-ssreflect.opam @@ -12,7 +12,7 @@ license: "CeCILL-B" build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] install: [ make "-C" "mathcomp/ssreflect" "install" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ] -depends: [ "coq" { ((>= "8.6" & < "8.9~") | (= "dev"))} ] +depends: [ "coq" { ((>= "8.6" & < "8.10~") | (= "dev"))} ] tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ] authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] |