diff options
Diffstat (limited to 'dev')
28 files changed, 85 insertions, 101 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-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/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh deleted file mode 100644 index 985c2db74e..0000000000 --- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then - - math_classes_CI_REF=program-mode-flag - math_classes_CI_GITURL=https://github.com/maximedenes/math-classes - - ltac2_CI_REF=program-mode-flag - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - - equations_CI_REF=thread-program - 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 diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg index cf9c5bd39a..4e1035f7b6 100644 --- a/dev/core_dune.dbg +++ b/dev/core_dune.dbg @@ -1,10 +1,10 @@ load_printer threads.cma load_printer str.cma -load_printer gramlib.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma +load_printer gramlib.cma load_printer byterun.cma load_printer kernel.cma load_printer library.cma diff --git a/dev/include b/dev/include index b982f4c9fa..c5de83b900 100644 --- a/dev/include +++ b/dev/include @@ -41,8 +41,6 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* cumulativity info *) ppcumulativity_info;; -#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index f588c20d02..2e8a7455de 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,17 @@ CODE=0 -# We assume that all merge commits are from the main branch +if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then + # The FIRST parent of bot merges is from the PR, the second is + # current master + head=$(git rev-parse HEAD~) +else + head=$(git rev-parse HEAD) +fi + +# We assume that all non-bot merge commits are from the main branch # For Coq it is extremely rare for this assumption to be broken -read -r base < <(git log -n 1 --merges --pretty='format:%H') -head=$(git rev-parse HEAD) +read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head") dev/lint-commits.sh "$base" "$head" || CODE=1 diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index 41392be5d7..ad60b1115f 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -42,7 +42,7 @@ OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) OVERLAY_FILE=$(mktemp overlay-XXXX) # Create the overlay file -printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then\n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" # We first try to build the contribs while test $# -gt 0 diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 813ad71be9..425f21de70 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -12,7 +12,8 @@ OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # Set SLOW_CONF to have the confirmation output wait for a newline # E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ -if [ -z ${SLOW_CONF+x} ]; then +# emacs doesn't send characters until the RET so we can't quick_conf +if [ -z ${SLOW_CONF+x} ] || [ -n "$INSIDE_EMACS" ]; then QUICK_CONF="-n 1" else QUICK_CONF="" diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index eab88c7290..a6ecec7e33 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -70,8 +70,6 @@ install_printer Top_printers.ppevar_universe_context install_printer Top_printers.ppconstraints install_printer Top_printers.ppuniverseconstraints install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval install_printer Top_printers.ppenv diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2629cf8626..a3d2f33216 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) -let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = let env = Global.env () in diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 4d874cdd12..cb32d2294c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppcumulativity_info : Univ.CumulativityInfo.t -> unit -val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit val ppuniverses : UGraph.t -> unit val ppnamedcontextval : Environ.named_context_val -> unit |