diff options
Diffstat (limited to 'dev/ci')
26 files changed, 192 insertions, 67 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 6663fbecf8..10b4f9b044 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -16,14 +16,12 @@ We are currently running tests on the following platforms: `./configure`. It should allow complying with this discipline without pain. -- Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. - - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. - Azure Pipelines is used to test the compilation of Coq and run the - test-suite on Windows. It is expected to replace appveyor eventually. + test-suite on Windows and on macOS. It is expected to replace + appveyor eventually. You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 470d07b27d..f26e0904bc 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -3,14 +3,15 @@ set -e -x APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c +NJOBS=2 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind ounit +opam install -j $NJOBS -y num ocamlfind ounit # Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..8dee465cf4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,11 +150,11 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology +# fiat_crypto_legacy ######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" ######################################################################## # coq_dpdgraph @@ -240,13 +240,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" @@ -273,3 +266,26 @@ : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" : "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" + +######################################################################## +# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft +######################################################################## +: "${struct_tact_CI_REF:=master}" +: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" +: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" + +: "${inf_seq_ext_CI_REF:=master}" +: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" +: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7e8013be9b..bba17314f7 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,5 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_TARGETS1="c-files printlite lite" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" + ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && make new-pipeline c-files ) + ulimit -s 32768 && \ + make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 12a70176c2..9ca8f76054 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -6,13 +6,6 @@ set -eo pipefail -function travis_fold { - if [ -n "${TRAVIS}" ]; - then - echo "travis_fold:$1:$2" - fi -} - CI_NAME="$1" CI_SCRIPT="ci-${CI_NAME}.sh" @@ -22,6 +15,5 @@ cd "${DIR}/../.." export TIMED=1 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log -travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log -travis_fold 'end' 'coq.test.timing' diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 386a3de204..5f819f31f9 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -26,12 +26,12 @@ if %ARCH% == 64 ( SET CYGROOT=C:\ci\cygwin%ARCH%
SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
CALL :MakeUniqueFolder %CYGROOT% CYGROOT
CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
SET COQREGTESTING=Y
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot
- REM addons with build issues
- REM -addon=vst ^
- REM -addon=aactactics ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix index 4c5cfd83da..3fcf177aec 100644 --- a/dev/ci/nix/CoLoR.nix +++ b/dev/ci/nix/CoLoR.nix @@ -1,5 +1,5 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; } diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix index 18c7750279..0d22a6b91b 100644 --- a/dev/ci/nix/Corn.nix +++ b/dev/ci/nix/Corn.nix @@ -1,5 +1,5 @@ { bignums, math-classes }: { - buildInputs = [ bignums math-classes ]; + coqBuildInputs = [ bignums math-classes ]; } diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix index a86fb2c44a..45d688285e 100644 --- a/dev/ci/nix/GeoCoq.nix +++ b/dev/ci/nix/GeoCoq.nix @@ -1,5 +1,5 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md index 1685b084e9..6f32abef95 100644 --- a/dev/ci/nix/README.md +++ b/dev/ci/nix/README.md @@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after changing the working directory to the root of the sources of that project, the contents of these variables can be evaluated to respectively set-up, build, and clean the project. + +## Variant: nocoq + +The dependencies of the third-party developments are split into `buildInputs` +and `coqBuildInputs`. The second list gathers the Coq libraries. In case you +only want the non-coq dependencies (because you want to use Coq from your `PATH`), +set the environment variable `NOCOQ` to some non-empty value. diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 4acfae48e4..277e9ee08f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -2,7 +2,8 @@ , branch , wd , project ? "xyz" -, bn ? "release" +, withCoq ? true +, bn ? "master" }: with pkgs; @@ -16,6 +17,11 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { name = "coq-git-mathcomp-git"; src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; }); in +let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { + inherit (mathcomp) src; + }); in +let coq-ext-lib = coqPackages.coq-ext-lib; in +let simple-io = coqPackages.simple-io; in let bignums = coqPackages.bignums.overrideAttrs (o: if bn == "release" then {} else if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else @@ -28,9 +34,17 @@ let math-classes = src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; }); in -let unicoq = callPackage ./unicoq.nix { inherit coq; }; in +let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; + }); in + +let unicoq = callPackage ./unicoq { inherit coq; }; in -let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in +let callPackage = newScope { inherit coq + bignums coq-ext-lib coqprime corn math-classes + mathcomp simple-io ssreflect unicoq; +}; in # Environments for building CI libraries with this Coq let projects = { @@ -45,12 +59,14 @@ let projects = { fiat_crypto = callPackage ./fiat_crypto.nix {}; fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; + formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; HoTT = callPackage ./HoTT.nix {}; math_classes = callPackage ./math_classes.nix {}; mathcomp = {}; mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; + quickchick = callPackage ./quickchick.nix {}; VST = callPackage ./VST.nix {}; }; in @@ -60,10 +76,16 @@ else let prj = projects."${project}"; in +let inherit (stdenv.lib) optional optionals; in + stdenv.mkDerivation { name = "shell-for-${project}-in-${branch}"; - buildInputs = [ coq ] ++ (prj.buildInputs or []); + buildInputs = + optional withCoq coq + ++ (prj.buildInputs or []) + ++ optionals withCoq (prj.coqBuildInputs or []) + ; configure = prj.configure or "true"; make = prj.make or "make"; diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 7b37e6e8e4..0f0ee91387 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ { coqprime }: { - buildInputs = [ coqprime ]; + coqBuildInputs = [ coqprime ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; make = "make new-pipeline c-files"; } diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix new file mode 100644 index 0000000000..53b9b1182b --- /dev/null +++ b/dev/ci/nix/formal-topology.nix @@ -0,0 +1,4 @@ +{ corn }: +{ + coqBuildInputs = [ corn ]; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix index b0fa2fe795..8edc3c8358 100644 --- a/dev/ci/nix/math_classes.nix +++ b/dev/ci/nix/math_classes.nix @@ -1,6 +1,6 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix index 9a2353c5cf..4acc326c02 100644 --- a/dev/ci/nix/mtac2.nix +++ b/dev/ci/nix/mtac2.nix @@ -1,5 +1,6 @@ { coq, unicoq }: { - buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ]; + coqBuildInputs = [ unicoq ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix index 3b8fdbab51..2341bb3173 100644 --- a/dev/ci/nix/oddorder.nix +++ b/dev/ci/nix/oddorder.nix @@ -1,4 +1,4 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; } diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix new file mode 100644 index 0000000000..46bf02ae3c --- /dev/null +++ b/dev/ci/nix/quickchick.nix @@ -0,0 +1,5 @@ +{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; + coqBuildInputs = [ ssreflect coq-ext-lib simple-io ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell index 2e4462ed40..a5f8ee8f54 100755 --- a/dev/ci/nix/shell +++ b/dev/ci/nix/shell @@ -17,4 +17,10 @@ else BN="" fi -nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN +if [ "$NOCOQ" ]; then + NOCOQ="--arg withCoq false" +else + NOCOQ="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META new file mode 100644 index 0000000000..30dd8b5559 --- /dev/null +++ b/dev/ci/nix/unicoq/META @@ -0,0 +1,2 @@ +archive(native) = "unicoq.cmxa" +plugin(native) = "unicoq.cmxs" diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq/default.nix index 093c262cde..36f40dbe33 100644 --- a/dev/ci/nix/unicoq.nix +++ b/dev/ci/nix/unicoq/default.nix @@ -4,8 +4,16 @@ stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; + patches = [ ./unicoq-num.patch ]; + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); configurePhase = "coq_makefile -f Make -o Makefile"; installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + postInstall = '' + install -d $OCAMLFIND_DESTDIR + ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/ + install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq + ''; } diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch new file mode 100644 index 0000000000..6d96d94dfc --- /dev/null +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -0,0 +1,44 @@ +commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b +Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> +Date: Thu Nov 29 08:59:22 2018 +0000 + + Make explicit dependency to num + +diff --git a/Make b/Make +index 550dc6a..8aa1309 100644 +--- a/Make ++++ b/Make +@@ -9,7 +9,7 @@ src/logger.ml + src/munify.mli + src/munify.ml + src/unitactics.mlg +-src/unicoq.mllib ++src/unicoq.mlpack + theories/Unicoq.v + test-suite/munifytest.v + test-suite/microtests.v +diff --git a/Makefile.local b/Makefile.local +new file mode 100644 +index 0000000..88be365 +--- /dev/null ++++ b/Makefile.local +@@ -0,0 +1 @@ ++CAMLPKGS += -package num +diff --git a/src/unicoq.mllib b/src/unicoq.mllib +deleted file mode 100644 +index 2b84e2d..0000000 +--- a/src/unicoq.mllib ++++ /dev/null +@@ -1,3 +0,0 @@ +-Logger +-Munify +-Unitactics +diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack +new file mode 100644 +index 0000000..2b84e2d +--- /dev/null ++++ b/src/unicoq.mlpack +@@ -0,0 +1,3 @@ ++Logger ++Munify ++Unitactics diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh new file mode 100644 index 0000000000..ebd1b524da --- /dev/null +++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then + + mtac2_CI_REF=proof-mode + mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 + + ltac2_CI_REF=proof-mode + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + equations_CI_REF=proof-mode + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi |