diff options
Diffstat (limited to 'dev')
33 files changed, 154 insertions, 64 deletions
diff --git a/dev/base_include b/dev/base_include index 96a867475d..45e79147c1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -129,7 +129,7 @@ open Elim open Equality open Hipattern open Inv -open Leminv +open Ltac_plugin.Leminv open Tacticals open Tactics open Eqschemes diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 6a740b9033..88d08a1724 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil ### Experimental automatic overlay creation and building If you break external projects that are hosted on GitHub, you can use -the `create-overlays.sh` script to automatically perform most of the +the `create_overlays.sh` script to automatically perform most of the above steps. In order to do so, call the script as: ``` -./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac +./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac ``` replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR number. The script will: diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 7b3e2703b8..64936cd236 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c +OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c 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 diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index c18e556da8..b87a9c0392 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,9 +46,9 @@ : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_REF:=master}" -: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" -: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" +: "${corn_CI_REF:=master}" +: "${corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}" ######################################################################## # Iris @@ -59,19 +59,19 @@ : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" -: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" +: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" +: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_REF:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" -: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" +: "${lambda_rust_CI_REF:=master}" +: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" +: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_REF:=master}" -: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" -: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" +: "${hott_CI_REF:=master}" +: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}" ######################################################################## # CoqHammer @@ -83,16 +83,23 @@ ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_REF:=master}" -: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" -: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" +: "${geocoq_CI_REF:=master}" +: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_REF:=master}" -: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" -: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" +: "${flocq_CI_REF:=master}" +: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" +: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}" + +######################################################################## +# coq-tools +######################################################################## +: "${coq_tools_CI_REF:=master}" +: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}" +: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}" ######################################################################## # Coquelicot @@ -242,7 +249,7 @@ # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" -: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}" : "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" ######################################################################## diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index 756f54dfbd..a21310cbd5 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download bignums -( cd "${CI_BUILD_DIR}/bignums" && make && make install) +( cd "${CI_BUILD_DIR}/bignums" && make && make install && cd tests && make) diff --git a/dev/ci/ci-coq_tools.sh b/dev/ci/ci-coq_tools.sh new file mode 100755 index 0000000000..9c95c49c9f --- /dev/null +++ b/dev/ci/ci-coq_tools.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coq_tools + +( cd "${CI_BUILD_DIR}/coq_tools" && make check || \ + { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 7d5d70cf90..ac3978dc8d 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Corn +git_download corn -( cd "${CI_BUILD_DIR}/Corn" && make && make install ) +( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross_crypto.sh index 900d12c1dd..900d12c1dd 100755 --- a/dev/ci/ci-cross-crypto.sh +++ b/dev/ci/ci-cross_crypto.sh diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext_lib.sh index 5eb167d97d..5eb167d97d 100755 --- a/dev/ci/ci-ext-lib.sh +++ b/dev/ci/ci-ext_lib.sh diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl_pcm.sh index cb951630c8..cb951630c8 100755 --- a/dev/ci/ci-fcsl-pcm.sh +++ b/dev/ci/ci-fcsl_pcm.sh diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat_crypto.sh index 811fefda35..811fefda35 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index e87483df0a..a3a704091b 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Flocq +git_download flocq -( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 8c57318477..e4fc983e68 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -5,6 +5,6 @@ ci_dir="$(dirname "$0")" install_ssralg -git_download GeoCoq +git_download geocoq -( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) +( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index c8e6fe690f..4b92c8cb4d 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download HoTT +git_download hott -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-lambda_rust.sh index d99e140bce..1ef0c2cb8f 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-lambda_rust.sh @@ -5,17 +5,17 @@ ci_dir="$(dirname "$0")" install_ssreflect -# Setup lambdaRust first -git_download lambdaRust +# Setup lambda_rust first +git_download lambda_rust # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris -git_download Iris +git_download iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp @@ -24,7 +24,7 @@ git_download stdpp ( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) # Build and validate Iris -( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) +( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) -# Build lambdaRust -( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) +# Build lambda_rust +( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math_classes.sh index ae31a8e7f8..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math_classes.sh diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-mathcomp.sh index cae127ee7b..cae127ee7b 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-mathcomp.sh diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple_io.sh index e7bcd80de7..e7bcd80de7 100755 --- a/dev/ci/ci-simple-io.sh +++ b/dev/ci/ci-simple_io.sh diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi_raft.sh index 3bcd52c464..3bcd52c464 100755 --- a/dev/ci/ci-verdi-raft.sh +++ b/dev/ci/ci-verdi_raft.sh diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e56e4d38ea..e240ea3ba1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-19-V29" +# CACHEKEY: "bionic_coq-V2020-03-13-V69" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" @@ -56,8 +56,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.09.1" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" +ENV COMPILER_EDGE="4.10.0" \ + BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index c8ea59f08a..b3ced999f6 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -22,7 +22,7 @@ let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { }); in let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: { - src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master"; + src = fetchTarball "https://github.com/coq-community/coq-ext-lib/tarball/master"; }); in let simple-io = diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh new file mode 100644 index 0000000000..e3a8eb07f3 --- /dev/null +++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then + + metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + metacoq_CI_GITURL=https://github.com/ejgallego/metacoq + + elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh new file mode 100644 index 0000000000..4170799be7 --- /dev/null +++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then + + elpi_CI_REF=partial-import + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh new file mode 100644 index 0000000000..cd6b408813 --- /dev/null +++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh @@ -0,0 +1,24 @@ +if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then + + coqhammer_CI_REF="evar-inst-list" + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + elpi_CI_REF="evar-inst-list" + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + equations_CI_REF="evar-inst-list" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + metacoq_CI_REF="evar-inst-list" + metacoq_CI_GITURL=https://github.com/ppedrot/metacoq + + mtac2_CI_REF="evar-inst-list" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + + quickchick_CI_REF="evar-inst-list" + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + unicoq_CI_REF="evar-inst-list" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + +fi diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh new file mode 100644 index 0000000000..6bee3c7bb6 --- /dev/null +++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then + + fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto + + mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 + + metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + metacoq_CI_GITURL=https://github.com/herbelin/template-coq + + unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + unimath_CI_GITURL=https://github.com/herbelin/UniMath + +fi diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh new file mode 100644 index 0000000000..b5faabcfe1 --- /dev/null +++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then + + elpi_CI_REF=no-mod-univs + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0506216541..8b0bf216e3 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -If you want to build the standard libraries and plugins you should -call `make -f Makefile.dune voboot`. It is usually enough to do that -once per-session. - More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. @@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and `coqide` in a fast build. In order to use them, do: ``` -$ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` @@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors: ## Dropping from coqtop: -After doing `make -f Makefile.dune voboot`, the following commands should work: +The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index eac8d86b0a..9498ab8bbb 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -9,6 +9,13 @@ ### ML API +Proof state and constant declaration: + +- A large consolidation of the API handling interactive and + non-interactive constant has been performed; low-level APIs are no + longer available, and the functionality of the `Proof_global` module + has been merged into `Declare`. + Notations: - Most operators on numerals have moved to file numTok.ml. @@ -68,7 +75,6 @@ Proof state: information related to the constant declaration. Some functions have been renamed from `start_proof` to `start_lemma` - Plugins that require access to the information about currently opened lemmas can add one of the `![proof]` attributes to their `mlg` entry, which will refine the type accordingly. See diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 556493ffad..d6348a3624 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.09.1))) -(context (opam (switch 4.09.1+flambda))) +(context (opam (switch 4.10.0))) +(context (opam (switch 4.10.0+flambda))) diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index b8a696ef21..fb84155392 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; - sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; + url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; + sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; }) diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 633913aac6..448e224f2e 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -16,6 +16,15 @@ then 1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting." fi +# Verify that the version of ocamlformat matches the one in .ocamlformat +# The following command will print an error message if that's not the case +# (and will print nothing if the versions match) +if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null +then + 1>&2 echo "Warning: Cannot check formatting." + ocamlformat=true +fi + 1>&2 echo "Auto fixing whitespace and formatting issues..." # We fix whitespace in the index and in the working tree @@ -43,7 +52,7 @@ if [ -s "$index" ]; then git apply --cached --whitespace=fix "$index" git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null git add -u 1>&2 echo #newline fi @@ -59,7 +68,7 @@ if [ -s "$tree" ]; then 1>&2 echo "Fixing unstaged changes..." git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null 1>&2 echo #newline fi diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index ddb0362186..666fb6cc91 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,4 @@ #!/usr/bin/env python3 -from __future__ import with_statement -from __future__ import print_function import os, re, sys, subprocess from io import open diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7002cbffac..00050a89e1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -59,8 +59,8 @@ let prrecarg = function let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) let get_current_context () = - try Vernacstate.Proof_global.get_current_context () - with Vernacstate.Proof_global.NoCurrentProof -> + try Vernacstate.Declare.get_current_context () + with Vernacstate.Declare.NoCurrentProof -> let env = Global.env() in Evd.from_env env, env [@@ocaml.warning "-3"] @@ -287,7 +287,7 @@ let constr_display csr = "LetIn("^(name_display na)^","^(term_display b)^"," ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" - | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")" + | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display (Array.of_list l))^")" | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")" | Ind ((sp,i),u) -> "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")" @@ -383,7 +383,7 @@ let print_pure_constr csr = Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{"; - Array.iter (fun x -> print_space (); box_display x) l; + List.iter (fun x -> print_space (); box_display x) l; print_string"}" | Const (c,u) -> print_string "Cons("; sp_con_display c; |