diff options
Diffstat (limited to 'dev')
37 files changed, 228 insertions, 180 deletions
diff --git a/dev/base_include b/dev/base_include index 48feeec147..b214959bad 100644 --- a/dev/base_include +++ b/dev/base_include @@ -1,24 +1,6 @@ - (* File to include to get some Coq facilities under the ocaml toplevel. This file is loaded by include *) -#cd".";; -#directory "parsing";; -#directory "interp";; -#directory "toplevel";; -#directory "library";; -#directory "kernel";; -#directory "gramlib";; -#directory "engine";; -#directory "pretyping";; -#directory "lib";; -#directory "proofs";; -#directory "tactics";; -#directory "printing";; -#directory "grammar";; -#directory "stm";; -#directory "vernac";; - #use "top_printers.ml";; #use "vm_printers.ml";; @@ -137,7 +119,6 @@ open Proof_global open Redexpr open Refiner open Tacmach -open Tactic_debug open Hints open Auto @@ -146,15 +127,9 @@ open Contradiction open Eauto open Elim open Equality -open Evar_tactics -open Extraargs -open Extratactics open Hipattern open Inv open Leminv -open Tacsubst -open Tacintern -open Tacinterp open Tacticals open Tactics open Eqschemes 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 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/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 01c32041d2..da91c85856 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -106,6 +106,16 @@ refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future. +## Dropping from coqtop: + +The following sequence is recommended: +``` +dune exec coqtop.byte +> Drop. +# #directory "dev";; +# #use "include_dune";; +``` + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index d05b6c8eef..60c0886896 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -92,7 +92,11 @@ ### These steps are the same for all releases (beta, final, patch-level) ### - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that - package managers can start preparing package updates. + package managers can start preparing package updates (including a + `coq-bignums` compatible version). +- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq` + (requires `coq-bignums` in `extra-dev` for a beta / in `released` + for a final release). - [ ] Draft a release on GitHub. - [ ] Get **@maximedenes** to sign the Windows and MacOS packages and upload them on GitHub. diff --git a/dev/inc_ltac b/dev/inc_ltac new file mode 100644 index 0000000000..8ef02445c2 --- /dev/null +++ b/dev/inc_ltac @@ -0,0 +1,7 @@ +open Evar_tactics +open Tactic_debug +open Tacsubst +open Tacintern +open Tacinterp +open Extraargs +open Extratactics diff --git a/dev/inc_ltac_dune b/dev/inc_ltac_dune new file mode 100644 index 0000000000..d7f505e8e0 --- /dev/null +++ b/dev/inc_ltac_dune @@ -0,0 +1,7 @@ +open Ltac_plugin__Evar_tactics +open Ltac_plugin__Tactic_debug +open Ltac_plugin__Tacsubst +open Ltac_plugin__Tacintern +open Ltac_plugin__Tacinterp +open Ltac_plugin__Extraargs +open Ltac_plugin__Extratactics diff --git a/dev/incdir b/dev/incdir new file mode 100644 index 0000000000..8ffd6bf6dc --- /dev/null +++ b/dev/incdir @@ -0,0 +1,16 @@ +#cd".";; +#directory "parsing";; +#directory "interp";; +#directory "toplevel";; +#directory "library";; +#directory "kernel";; +#directory "gramlib";; +#directory "engine";; +#directory "pretyping";; +#directory "lib";; +#directory "proofs";; +#directory "tactics";; +#directory "printing";; +#directory "grammar";; +#directory "stm";; +#directory "vernac";; diff --git a/dev/incdir_dune b/dev/incdir_dune new file mode 100644 index 0000000000..9d0fee1fa2 --- /dev/null +++ b/dev/incdir_dune @@ -0,0 +1,16 @@ +#cd".";; +#directory "_build/default/lib/.lib.objs/";; +#directory "_build/default/clib/.clib.objs/";; +#directory "_build/default/kernel/.kernel.objs/";; +#directory "_build/default/library/.library.objs/";; +#directory "_build/default/engine/.engine.objs/";; +#directory "_build/default/pretyping/.pretyping.objs/";; +#directory "_build/default/interp/.interp.objs/";; +#directory "_build/default/parsing/.parsing.objs/";; +#directory "_build/default/gramlib/.gramlib.objs/";; +#directory "_build/default/proofs/.proofs.objs/";; +#directory "_build/default/tactics/.tactics.objs/";; +#directory "_build/default/printing/.printing.objs/";; +#directory "_build/default/vernac/.vernac.objs/";; +#directory "_build/default/stm/.stm.objs/";; +#directory "_build/default/toplevel/.toplevel.objs/";; diff --git a/dev/include b/dev/include index b982f4c9fa..fa4bf827d7 100644 --- a/dev/include +++ b/dev/include @@ -1,4 +1,3 @@ - (* File to include to install the pretty-printers in the ocaml toplevel *) (* Typical usage : @@ -15,71 +14,8 @@ then ignore (Toploop.use_silently Format.std_formatter "dev/include") *) -(* For OCaml 3.10.x: - clflags.cmi (a ocaml compilation by-product) must be in the library path. - On Debian, install ocaml-compiler-libs, and uncomment the following: - #directory "+compiler-libs/utils";; - Clflags.recursive_types := true;; -*) - #cd ".";; +#use "incdir";; #use "base_include";; - -#install_printer (* pp_stdcmds *) pp;; - -#install_printer (* pattern *) pppattern;; -#install_printer (* glob_constr *) ppglob_constr;; -#install_printer (* open constr *) ppopenconstr;; -#install_printer (* constr *) ppconstr;; -#install_printer (* econstr *) ppeconstr;; -#install_printer (* constr_substituted *) ppsconstr;; -#install_printer (* constraints *) ppconstraints;; -#install_printer (* univ constraints *) ppuniverseconstraints;; -#install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverses;; -#install_printer (* univ level *) ppuni_level;; -#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;; -#install_printer (* univ full subst *) ppuniverse_level_subst;; -#install_printer (* univ opt subst *) ppuniverse_opt_subst;; -#install_printer (* evar univ ctx *) ppevar_universe_context;; -#install_printer (* inductive *) ppind;; -#install_printer (* 'a scheme_kind *) ppscheme;; -#install_printer (* type_judgement *) pptype;; -#install_printer (* judgement *) ppj;; -#install_printer (* id set *) ppidset;; -#install_printer (* int set *) ppintset;; - -#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; -#install_printer (* Reductionops machine stack *) pp_stack_t;; - -(*#install_printer (* hint_db *) print_hint_db;;*) -(*#install_printer (* hints_path *) pphintspath;;*) -#install_printer (* goal *) ppgoal;; -(*#install_printer (* sigma goal *) ppsigmagoal;;*) -#install_printer (* proof *) pproof;; -#install_printer (* Goal.goal *) ppgoalgoal;; -#install_printer (* proofview *) ppproofview;; -#install_printer (* metaset.t *) ppmetas;; -#install_printer (* evar *) ppevar;; -#install_printer (* evar_map *) ppevm;; -#install_printer (* Evar.Set.t *) ppexistentialset;; -#install_printer (* clenv *) ppclenv;; -#install_printer (* env *) ppenv;; -#install_printer (* Hint_db.t *) pphintdb;; -#install_printer (* named_context_val *) ppnamedcontextval;; - -#install_printer (* tactic *) pptac;; -#install_printer (* object *) ppobj;; -#install_printer (* global_reference *) ppglobal;; -#install_printer (* generic_argument *) pp_generic_argument;; - -#install_printer (* fconstr *) ppfconstr;; - -#install_printer (* Future.computation *) ppfuture;; +#use "inc_ltac";; +#use "include_printers";; diff --git a/dev/include_dune b/dev/include_dune new file mode 100644 index 0000000000..2ef8eb4d04 --- /dev/null +++ b/dev/include_dune @@ -0,0 +1,22 @@ +(* File to include to install the pretty-printers in the ocaml toplevel *) + +(* Typical usage : + + $ dune exec coqtop.byte # or even better : rlwrap coqtop.byte + Coq < Drop. + # #directory "dev";; + # #use "include";; + + Alternatively, you can avoid typing #use "include" after each Drop + by adding the following lines in your $HOME/.ocamlinit : + + #directory "+compiler-libs";; + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "dev/include") +*) + +#cd ".";; +#use "incdir_dune";; +#use "base_include";; +#use "inc_ltac_dune";; +#use "include_printers";; diff --git a/dev/include_printers b/dev/include_printers new file mode 100644 index 0000000000..90088e40bf --- /dev/null +++ b/dev/include_printers @@ -0,0 +1,55 @@ +#install_printer (* pp_stdcmds *) pp;; +#install_printer (* pattern *) pppattern;; +#install_printer (* glob_constr *) ppglob_constr;; +#install_printer (* open constr *) ppopenconstr;; +#install_printer (* constr *) ppconstr;; +#install_printer (* econstr *) ppeconstr;; +#install_printer (* constr_substituted *) ppsconstr;; +#install_printer (* constraints *) ppconstraints;; +#install_printer (* univ constraints *) ppuniverseconstraints;; +#install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverses;; +#install_printer (* univ level *) ppuni_level;; +#install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; +#install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* univ set *) ppuniverse_set;; +#install_printer (* univ instance *) ppuniverse_instance;; +#install_printer (* univ subst *) ppuniverse_subst;; +#install_printer (* univ full subst *) ppuniverse_level_subst;; +#install_printer (* univ opt subst *) ppuniverse_opt_subst;; +#install_printer (* evar univ ctx *) ppevar_universe_context;; +#install_printer (* inductive *) ppind;; +#install_printer (* 'a scheme_kind *) ppscheme;; +#install_printer (* type_judgement *) pptype;; +#install_printer (* judgement *) ppj;; +#install_printer (* id set *) ppidset;; +#install_printer (* int set *) ppintset;; + +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; + +(*#install_printer (* hint_db *) print_hint_db;;*) +(*#install_printer (* hints_path *) pphintspath;;*) +#install_printer (* goal *) ppgoal;; +(*#install_printer (* sigma goal *) ppsigmagoal;;*) +#install_printer (* proof *) pproof;; +#install_printer (* Goal.goal *) ppgoalgoal;; +#install_printer (* proofview *) ppproofview;; +#install_printer (* metaset.t *) ppmetas;; +#install_printer (* evar *) ppevar;; +#install_printer (* evar_map *) ppevm;; +#install_printer (* Evar.Set.t *) ppexistentialset;; +#install_printer (* clenv *) ppclenv;; +#install_printer (* env *) ppenv;; +#install_printer (* Hint_db.t *) pphintdb;; +#install_printer (* named_context_val *) ppnamedcontextval;; + +#install_printer (* tactic *) pptac;; +#install_printer (* object *) ppobj;; +#install_printer (* global_reference *) ppglobal;; +#install_printer (* generic_argument *) pp_generic_argument;; + +#install_printer (* fconstr *) ppfconstr;; + +#install_printer (* Future.computation *) ppfuture;; 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 5eac3e2b9c..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 @@ -161,6 +159,7 @@ val ppobj : Libobject.obj -> unit val cast_kind_display : Constr.cast_kind -> string val constr_display : Constr.constr -> unit val print_pure_constr : Constr.types -> unit +val print_pure_econstr : EConstr.types -> unit val pploc : Loc.t -> unit |