diff options
Diffstat (limited to 'dev/ci')
20 files changed, 72 insertions, 75 deletions
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh index c0030c566f..04c7d5db91 100755 --- a/dev/ci/azure-build.sh +++ b/dev/ci/azure-build.sh @@ -4,6 +4,4 @@ set -e -x cd $(dirname $0)/../.. -./configure -local -make -j 2 byte -make -j 2 world +make -f Makefile.dune coq coqide-server diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 8a1e36659c..9448a03f4f 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -10,4 +10,4 @@ bash opam64/install.sh opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind ounit +opam install -y num ocamlfind dune ounit diff --git a/dev/ci/azure-test.sh b/dev/ci/azure-test.sh index 8813245e5a..80a3d2e083 100755 --- a/dev/ci/azure-test.sh +++ b/dev/ci/azure-test.sh @@ -4,6 +4,5 @@ set -e -x #NB: if we make test-suite from the main makefile we get environment #too large for exec error -cd $(dirname $0)/../../test-suite -make -j 2 clean -make -j 2 PRINT_LOGS=1 +cd $(dirname $0)/../../ +make -f Makefile.dune test-suite diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 5205946261..2ac78d3c2b 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a5aa54144c..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -62,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" if [ -d "$DEST" ]; then echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" git clone "$GITURL" "$DEST" cd "$DEST" git checkout "$REF" else # When possible, we download tarballs to reduce bandwidth and latency local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" local ARCHIVEURL="${!ARCHIVEURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" mkdir -p "$DEST" cd "$DEST" - wget "$ARCHIVEURL/$REF.tar.gz" - tar xvfz "$REF.tar.gz" --strip-components=1 - rm -f "$REF.tar.gz" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4cd7faf757..43278c37b1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-01-28-V1" +# CACHEKEY: "bionic_coq-V2019-02-17-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" -RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE - # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 277e9ee08f..94e0a666e2 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -39,11 +39,21 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; }); in +let stdpp = coqPackages.stdpp.overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2"; + }); in + +let iris = (coqPackages.iris.override { inherit coq stdpp; }) + .overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2"; + propagatedBuildInputs = [ stdpp ]; + }); in + let unicoq = callPackage ./unicoq { inherit coq; }; in let callPackage = newScope { inherit coq - bignums coq-ext-lib coqprime corn math-classes - mathcomp simple-io ssreflect unicoq; + bignums coq-ext-lib coqprime corn iris math-classes + mathcomp simple-io ssreflect stdpp unicoq; }; in # Environments for building CI libraries with this Coq @@ -62,6 +72,8 @@ let projects = { formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; HoTT = callPackage ./HoTT.nix {}; + iris = callPackage ./iris.nix {}; + lambda-rust = callPackage ./lambda-rust.nix {}; math_classes = callPackage ./math_classes.nix {}; mathcomp = {}; mtac2 = callPackage ./mtac2.nix {}; diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix new file mode 100644 index 0000000000..b55cccc7c6 --- /dev/null +++ b/dev/ci/nix/iris.nix @@ -0,0 +1,4 @@ +{ stdpp }: +{ + coqBuildInputs = [ stdpp ]; +} diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix new file mode 100644 index 0000000000..0d07c3028a --- /dev/null +++ b/dev/ci/nix/lambda-rust.nix @@ -0,0 +1,4 @@ +{ iris }: +{ + coqBuildInputs = [ iris ]; +} diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META deleted file mode 100644 index 30dd8b5559..0000000000 --- a/dev/ci/nix/unicoq/META +++ /dev/null @@ -1,2 +0,0 @@ -archive(native) = "unicoq.cmxa" -plugin(native) = "unicoq.cmxs" diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix index 36f40dbe33..54c67ac0fd 100644 --- a/dev/ci/nix/unicoq/default.nix +++ b/dev/ci/nix/unicoq/default.nix @@ -1,4 +1,10 @@ -{ stdenv, coq }: +{ stdenv, writeText, coq }: + +let META = writeText "META" '' + archive(native) = "unicoq.cmxa" + plugin(native) = "unicoq.cmxs" +''; in + stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; @@ -12,8 +18,9 @@ stdenv.mkDerivation { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; postInstall = '' + cp ${META} META 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 + install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq ''; } diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh deleted file mode 100644 index 6e89741e29..0000000000 --- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then - - bignums_CI_REF=primitive-integers - bignums_CI_GITURL=https://github.com/vbgl/bignums - - mtac2_CI_REF=primitive-integers - mtac2_CI_GITURL=https://github.com/vbgl/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh deleted file mode 100644 index 2df8affd14..0000000000 --- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then - - elpi_CI_REF=ltac+remove_aliases - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh deleted file mode 100644 index f2a113b118..0000000000 --- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then - - mtac2_CI_REF=build+warn_50 - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh deleted file mode 100644 index f532fdfc52..0000000000 --- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then - - ltac2_CI_REF=proof_rework - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - mtac2_CI_REF=proof_rework - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh new file mode 100644 index 0000000000..23eb24c304 --- /dev/null +++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then + + ltac2_CI_REF=proofview+proof_info + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + fiat_parsers_CI_REF=proofview+proof_info + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh deleted file mode 100644 index efcdd2e97f..0000000000 --- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then - - paramcoq_CI_REF=stm-shallow-logic - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh deleted file mode 100644 index ebd1b524da..0000000000 --- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh +++ /dev/null @@ -1,12 +0,0 @@ -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 diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi |