diff options
Diffstat (limited to 'dev')
55 files changed, 556 insertions, 1122 deletions
diff --git a/dev/README b/dev/README deleted file mode 100644 index 453f85f0d6..0000000000 --- a/dev/README +++ /dev/null @@ -1,50 +0,0 @@ -This directory contains information and tools to help develop the - Coq system - ====================== - - -Debugging and profiling (in current directory - see doc/debugging.txt) ------------------------ - -ocamldebug-coq: to launch ocaml debugger (generated by the configure script) - -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger - -include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) -base_include: to install raw pretty-printers from ocaml toplevel - -vm_printers.ml, top_printers.ml: ML pretty-printers for debugging - - -Miscellaneous information about the code (directory doc) ------------------------------------------ - -changes.md: (partial) per-version summary of the evolution of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.md: help for debugging or profiling -universes.txt: help for debugging universes -translate.txt: help for using coq translator -extensions.txt: some help about TACTIC EXTEND - -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation - - -Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) ----------------------------------------- -"make mli-doc" in coq root directory. - - -Other development tools (directory tools) ------------------------ - -coqdev.el: helper customizations for everyday Coq development, eg - making `compile' work in subdirectories - -objects.el: various development utilities at emacs level - -anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse - location of Anomaly backtraces and jump to them conveniently from - the Emacs *compilation* output. diff --git a/dev/README.md b/dev/README.md new file mode 100644 index 0000000000..4642aaf06d --- /dev/null +++ b/dev/README.md @@ -0,0 +1,46 @@ +# This directory contains information and tools to help develop the Coq system + + +## Debugging and profiling (`dev/`) +**More info on debugging: [`doc/debugging.md`](doc/debugging.md)** + +| File | Description | +| ---- | ----------- | +| dev/ocamldebug-coq | To launch ocaml debugger (generated by the configure script) | +| dev/db | To install pretty-printers from ocaml debugger | +| dev/base_db | To install raw pretty-printers from ocaml debugger | +| dev/include | To install pretty-printers from ocaml toplevel (use with the coq Drop command) | +| dev/base_include | To install raw pretty-printers from ocaml toplevel | +| dev/vm_printers.ml, top_printers.ml | ML pretty-printers for debugging | + + +## Miscellaneous information about the code (`dev/doc`) +**Beginner's guide to hacking Coq: [`dev/doc/README.md`](doc/README.md)** + +| File | Description | +| ---- | ----------- | +| [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | +| [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | +| [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | +| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | +| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | +| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation | +| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | +| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | +| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate | +| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | +| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | + + +## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`) +`make mli-doc` in coq root directory. + + +## Other development tools (`dev/tools`) + +| File | Description | +| ---- | ----------- | +| [`dev/tools/coqdev.el`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories +| [`dev/tools/objects.el`](tools/objects.el) | Various development utilities at emacs level | diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 94e90bf4fe..60108cda4f 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -793,7 +793,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -933,7 +933,7 @@ function make_camlp5 { make_ocaml make_findlib - if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then + if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile @@ -1387,12 +1387,12 @@ function make_coq_installer { # Provides BigN, BigZ, BigQ that used to be part of Coq standard library function make_addon_bignums { - bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_BRANCH" | cut -f 1) + bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1) if [[ "$bignums_SHA" == "" ]]; then - # $bignums_CI_BRANCH must have been a tag and not a branch - bignums_SHA="$bignums_CI_BRANCH" + # $bignums_CI_REF must have been a tag / commit and not a branch + bignums_SHA="$bignums_CI_REF" fi - if build_prep "${bignums_CI_GITURL}/archive" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then + if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1405,12 +1405,12 @@ function make_addon_bignums { # A new (experimental) tactic language function make_addon_ltac2 { - ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_BRANCH" | cut -f 1) + ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1) if [[ "$ltac2_SHA" == "" ]]; then - # $ltac2_CI_BRANCH must have been a tag and not a branch - ltac2_SHA="$ltac2_CI_BRANCH" + # $ltac2_CI_REF must have been a tag / commit and not a branch + ltac2_SHA="$ltac2_CI_REF" fi - if build_prep "${ltac2_CI_GITURL}/archive" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then + if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then log1 make all log2 make install build_post @@ -1421,12 +1421,12 @@ function make_addon_ltac2 { # A function definition plugin function make_addon_equations { - Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_BRANCH" | cut -f 1) + Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1) if [[ "$Equations_SHA" == "" ]]; then - # $Equations_CI_BRANCH must have been a tag and not a branch - Equations_SHA="$Equations_CI_BRANCH" + # $Equations_CI_REF must have been a tag / commit and not a branch + Equations_SHA="$Equations_CI_REF" fi - if build_prep "${Equations_CI_GITURL}/archive" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then + if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then # Note: PATH is autmatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile diff --git a/dev/ci/README.md b/dev/ci/README.md index 45176581cd..a814e4914e 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -75,9 +75,6 @@ We are currently running tests on the following platforms: camlp5, and with warnings as errors; it runs the test-suite and tests the compilation of several external developments. -- Circle CI runs tests that are redundant with GitLab CI and may be removed - eventually. - - Travis CI is used to test the compilation of Coq and run the test-suite on macOS. It also runs a linter that checks whitespace discipline. A [pre-commit hook](../tools/pre-commit) is automatically installed by @@ -141,14 +138,11 @@ persists to and is used by the next jobs. Artifacts can also be downloaded from the GitLab repository. Currently, available artifacts are: -- the Coq executables and stdlib, in three copies varying in +- the Coq executables and stdlib, in four copies varying in architecture and OCaml version used to build Coq. -- the Coq documentation, built only in the `build:base` job. When submitting +- the Coq documentation, built in the `documentation` job. When submitting a documentation PR, this can help reviewers checking the rendered result. -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. - ### GitLab and Windows If your repository has access to runners tagged `windows`, setting the @@ -165,8 +159,7 @@ automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify -the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml), +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) and [`Dockerfile`](docker/bionic_coq/Dockerfile) The Docker building job reuses the uploaded image if it is available, diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 7bf9ad8c9b..d2176e326c 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,7 +2,7 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c +APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/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 28321d13e2..63d5541f48 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -9,124 +9,147 @@ ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_BRANCH:=master}" +: "${mathcomp_CI_REF:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" -: "${oddorder_CI_BRANCH:=master}" +: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" + +: "${oddorder_CI_REF:=master}" : "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" +: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" ######################################################################## # UniMath ######################################################################## -: "${UniMath_CI_BRANCH:=master}" +: "${UniMath_CI_REF:=master}" : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_BRANCH:=master}" +: "${unicoq_CI_REF:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" +: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_REF:=master-sync}" : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" +: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_BRANCH:=master}" -: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes}" +: "${math_classes_CI_REF:=master}" +: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" +: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_BRANCH:=master}" -: "${Corn_CI_GITURL:=https://github.com/c-corn/corn}" +: "${Corn_CI_REF:=master}" +: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_BRANCH:=master}" +: "${stdpp_CI_REF:=master}" : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_BRANCH:=master}" +: "${Iris_CI_REF:=master}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_BRANCH:=master}" +: "${lambdaRust_CI_REF:=master}" : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_BRANCH:=master}" +: "${HoTT_CI_REF:=master}" : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## # Ltac2 ######################################################################## -: "${ltac2_CI_BRANCH:=master}" +: "${ltac2_CI_REF:=master}" : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" +: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_BRANCH:=master}" +: "${GeoCoq_CI_REF:=master}" : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_BRANCH:=master}" +: "${Flocq_CI_REF:=master}" : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" +: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" ######################################################################## # Coquelicot ######################################################################## -: "${Coquelicot_CI_BRANCH:=master}" +: "${Coquelicot_CI_REF:=master}" : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_BRANCH:=master}" +: "${CompCert_CI_REF:=master}" : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_BRANCH:=master}" +: "${VST_CI_REF:=master}" : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" ######################################################################## # cross-crypto ######################################################################## -: "${cross_crypto_CI_BRANCH:=master}" +: "${cross_crypto_CI_REF:=master}" : "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" +: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" ######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_BRANCH:=master}" +: "${fiat_parsers_CI_REF:=master}" : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" +: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_BRANCH:=master}" +: "${fiat_crypto_CI_REF:=master}" : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## # formal-topology ######################################################################## -: "${formal_topology_CI_BRANCH:=ci}" +: "${formal_topology_CI_REF:=ci}" : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" +: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-master}" +: "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" +: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_BRANCH:=master}" +: "${CoLoR_CI_REF:=master}" : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" +: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" ######################################################################## # SF @@ -138,53 +161,68 @@ ######################################################################## # TLC ######################################################################## -: "${tlc_CI_BRANCH:=master}" +: "${tlc_CI_REF:=master}" : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_BRANCH:=master}" +: "${bignums_CI_REF:=master}" : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" +: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_REF:=master}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" +: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=master}" +: "${Equations_CI_REF:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_BRANCH:=coq-master}" +: "${Elpi_CI_REF:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_REF:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" +: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## # pidetop ######################################################################## -: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_REF:=v8.9}" : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" +: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" ######################################################################## # ext-lib ######################################################################## -: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_REF:=master}" : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" +: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" + +######################################################################## +# simple-io +######################################################################## +: "${simple_io_CI_REF:=master}" +: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" +: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_REF:=master}" : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" +: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 447076e092..5205946261 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" +FORCE_GIT=1 +git_download bedrock2 -git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" -( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${bedrock2_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index 0082919679..756f54dfbd 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi +git_download bignums -bignums_CI_DIR="${CI_BUILD_DIR}/Bignums" - -git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}" - -( cd "${bignums_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/bignums" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 8ce5f2418f..dc696f69d9 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CoLoR_CI_DIR=${CI_BUILD_DIR}/color +git_download CoLoR -# Compile CoLoR -git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}" -( cd "${CoLoR_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/CoLoR" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 85df249d38..3536cc70b2 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,10 +20,6 @@ else then export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" export CI_BRANCH="$TRAVIS_BRANCH" - elif [ -n "${CIRCLECI}" ]; - then - export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" - export CI_BRANCH="$CIRCLE_BRANCH" else # assume local CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH @@ -38,7 +34,7 @@ export COQBIN="$COQBIN/" ls "$COQBIN" -# Where we clone and build external developments +# Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" # shellcheck source=ci-basic-overlay.sh @@ -48,29 +44,38 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do . "${overlay}" done -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" - -# git_checkout branch url dest will create a git repository -# in <dest> (if it does not exist already) and checkout the -# remote branch <branch> from <url> -git_checkout() +# [git_download project] will download [project] and unpack it +# in [$CI_BUILD_DIR/project] if the folder does not exist already; +# if it does, it will do nothing except print a warning (this can be +# useful when building locally). +# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty +# (local build), it uses git clone to perform the download. +git_download() { - local _BRANCH=${1} - local _URL=${2} - local _DEST=${3} - - # Allow an optional 4th argument for the commit - local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=() - if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi - - mkdir -p "${_DEST}" - ( cd "${_DEST}" && \ - if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ - echo "Checking out ${_DEST}" && \ - git fetch "${_URL}" "${_BRANCH}" && \ - git checkout "${_COMMIT}" && \ - echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) + local PROJECT=$1 + local DEST="$CI_BUILD_DIR/$PROJECT" + + 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" + fi } make() @@ -88,31 +93,27 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + echo 'Installing ssreflect' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq ssreflect/all_ssreflect.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssr.install\\r' - } # this installs just the ssreflect + algebra library of math-comp install_ssralg() { - echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + echo 'Installing ssralg' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq algebra/all_algebra.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssralg.install\\r' - } diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 8d490591b6..01c35ceb4a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" +git_download CompCert -git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" - -( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd "${CI_BUILD_DIR}/CompCert" && \ + ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index 5d57fce1c7..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph" +git_download coq_dpdgraph -git_checkout "${coq_dpdgraph_CI_BRANCH}" "${coq_dpdgraph_CI_GITURL}" "${coq_dpdgraph_CI_DIR}" - -( cd "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite ) +( cd "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index d86d61ef6a..5d8817491d 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,10 +3,9 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot" - install_ssreflect -git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}" +FORCE_GIT=1 +git_download Coquelicot -( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 9298fc70af..7d5d70cf90 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Corn_CI_DIR="${CI_BUILD_DIR}/corn" +git_download Corn -git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}" - -( cd "${Corn_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Corn" && make && make install ) diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh index a0d3aa6551..900d12c1dd 100755 --- a/dev/ci/ci-cross-crypto.sh +++ b/dev/ci/ci-cross-crypto.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto" +FORCE_GIT=1 +git_download cross_crypto -git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}" -( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${cross_crypto_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 9c58034be1..9b4a06fd5b 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Elpi_CI_DIR="${CI_BUILD_DIR}/elpi" +git_download Elpi -git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}" - -( cd "${Elpi_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 98735b4ec4..998d50faa7 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Equations_CI_DIR="${CI_BUILD_DIR}/Equations" +git_download Equations -git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}" - -( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) +( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ + make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh index cf212c2fb5..5eb167d97d 100755 --- a/dev/ci/ci-ext-lib.sh +++ b/dev/ci/ci-ext-lib.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi +git_download ext_lib -ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib" - -git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}" - -( cd "${ext_lib_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/ext_lib" && make && make install) diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh index fdc4c729b6..cb951630c8 100755 --- a/dev/ci/ci-fcsl-pcm.sh +++ b/dev/ci/ci-fcsl-pcm.sh @@ -3,10 +3,8 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm" - install_ssreflect -git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}" +git_download fcsl_pcm -( cd "${fcsl_pcm_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh new file mode 100755 index 0000000000..e0395754e5 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto + +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 && \ + 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 48a1366aba..7e8013be9b 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,12 +3,12 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" +FORCE_GIT=1 +git_download fiat_crypto -git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" +# We need a larger stack size to not overflow ocamlopt+flambda when +# building the executables. +# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 -( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) - -fiat_crypto_CI_TARGETS1="printlite lite lite-display" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + ulimit -s 32768 && make new-pipeline c-files ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 35c2284050..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat" +FORCE_GIT=1 +git_download fiat_parsers -git_checkout "${fiat_parsers_CI_BRANCH}" "${fiat_parsers_CI_GITURL}" "${fiat_parsers_CI_DIR}" - -( cd "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core ) +( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 8599e4d50e..e87483df0a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Flocq_CI_DIR="${CI_BUILD_DIR}/flocq" +git_download Flocq -git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}" - -( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 118d151500..8be5a06ed2 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology" +git_download formal_topology -git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}" - -( cd "${formal_topology_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 24cd9c4272..8c57318477 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,10 +3,8 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" - -git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" - install_ssralg -( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) +git_download GeoCoq + +( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 6ded97984e..7eeeb09372 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT +git_download HoTT -git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" - -( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 1af0f634c4..6960a8b98a 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -3,32 +3,28 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp" -Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq" -lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust" - install_ssreflect # Setup lambdaRust first -git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" +git_download lambdaRust # Extract required version of Iris -Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" +git_download Iris # Extract required version of std++ -stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" +git_download stdpp # Build std++ -( cd "${stdpp_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) -# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris -( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install ) +# Build and validate Iris +( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) # Build lambdaRust -( cd "${lambdaRust_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 5981aaaae7..4df22bf249 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2" +git_download ltac2 -git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}" - -( cd "${ltac2_CI_DIR}" && make && make tests && make install ) +( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 6a064b2971..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" +git_download math_classes -git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" - -( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) +( cd "${CI_BUILD_DIR}/math_classes" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 20328baf2a..a74f9fa4d3 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,11 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" -oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" +git_download mathcomp -git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" -git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) -( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) -( cd "${oddorder_CI_DIR}/" && make ) +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 1372acb8e5..7075d4d7f6 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,17 +3,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 +git_download unicoq -# Setup UniCoq +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) -git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" +git_download mtac2 -( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install ) - -# Setup MetaCoq - -git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}" - -( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index 32cba0808e..d22b9c8f7c 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -1,12 +1,9 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" - -git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" +git_download pidetop # Travis / Gitlab have different filesystem layout due to use of # `-local`. We need to improve this divergence but if we use Dune this @@ -17,6 +14,6 @@ else COQLIB="$COQBIN/../" fi -( cd "${pidetop_CI_DIR}" && jbuilder build @install ) +( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install ) -echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds +echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh index fc39e2685d..08686d7ced 100755 --- a/dev/ci/ci-quickchick.sh +++ b/dev/ci/ci-quickchick.sh @@ -1,18 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" - -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi - -quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick" +. "${ci_dir}/ci-common.sh" install_ssreflect -git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" +git_download quickchick -( cd "${quickchick_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh new file mode 100755 index 0000000000..e7bcd80de7 --- /dev/null +++ b/dev/ci/ci-simple-io.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download simple_io + +( cd "${CI_BUILD_DIR}/simple_io" && make build && make install) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh deleted file mode 100755 index e77a553047..0000000000 --- a/dev/ci/ci-template.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -Template_CI_BRANCH=master -Template_CI_GITURL=https://github.com/Template/Template -Template_CI_DIR="${CI_BUILD_DIR}/Template" - -git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}" - -( cd "${Template_CI_DIR}" && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 31387c8ddc..a2f0bea555 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -tlc_CI_DIR="${CI_BUILD_DIR}/tlc" +FORCE_GIT=1 +git_download tlc -git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}" - -( cd "${tlc_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/tlc" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index aa20fe1ff0..a7644fee23 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" +git_download UniMath -git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" - -( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) +( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 7a097eaab4..0fec19205a 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -VST_CI_DIR="${CI_BUILD_DIR}/VST" +git_download VST -git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" - -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 52f851917e..7a649591dd 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-06-13-V1" +# CACHEKEY: "bionic_coq-V2018-08-27-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -6,10 +6,12 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" -RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ +RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ + m4 automake autoconf time wget rsync git gcc-multilib opam \ libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ + python3-setuptools python3-wheel python3-pip RUN pip3 install antlr4-python3-runtime @@ -26,8 +28,8 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # 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.0 jbuilder.1.0+beta20 ounit.2.0.8" \ - CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \ + CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ @@ -41,8 +43,8 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch -ENV COMPILER_EDGE="4.06.1" \ - CAMLP5_VER_EDGE="7.05" \ +ENV COMPILER_EDGE="4.07.0" \ + CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index e6a2c4460b..d812df3ec0 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,6 +1,6 @@ #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 0000000000..575df07425 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/07863-rm-sorts-contents.sh b/dev/ci/user-overlays/07863-rm-sorts-contents.sh deleted file mode 100644 index 374a614848..0000000000 --- a/dev/ci/user-overlays/07863-rm-sorts-contents.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7863" ] || [ "$CI_BRANCH" = "rm-sorts-contents" ]; then - Elpi_CI_BRANCH=fix-sorts-contents - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/07906-univs-of-constr.sh b/dev/ci/user-overlays/07906-univs-of-constr.sh deleted file mode 100644 index 0716650879..0000000000 --- a/dev/ci/user-overlays/07906-univs-of-constr.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7906" ] || [ "$CI_BRANCH" = "univs-of-constr-noseff" ]; then - Equations_CI_BRANCH=fix-univs-of-constr - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git - - Elpi_CI_BRANCH=fix-universes-of-constr - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 11e4d9ae09..68afe7ee4a 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,12 @@ request to test it with the adapted version of the external project. An overlay is a file which defines where to look for the patched version so that testing is possible. It redefines some variables from [`ci-basic-overlay.sh`](../ci-basic-overlay.sh): -give the name of your branch using a `_CI_BRANCH` variable and the location of -your fork using a `_CI_GITURL` variable. +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. +The `_CI_GITURL` variable should be the URL of the repository without a +trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -23,7 +27,7 @@ Example: `00669-maximedenes-ssr-merge.sh` containing #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/doc/README.md b/dev/doc/README.md new file mode 100644 index 0000000000..223cf6286e --- /dev/null +++ b/dev/doc/README.md @@ -0,0 +1,77 @@ +# Beginner's guide to hacking Coq + +## Getting dependencies + +Assuming one is running Ubuntu (if not, replace `apt` with the package manager of choice) + +``` +$ sudo apt-get install make opam git + +# At the time of writing, <latest-ocaml-version> is 4.07.0. +# The latest version number is available at: https://ocaml.org/releases/ + +$ opam init --comp <latest-ocaml-version> + +# Then follow the advice displayed at the end as how to update your + ~/.bashrc and ~/.ocamlinit files. + +$ source ~/.bashrc +$ opam install camlp5 + +# needed if you want to build "coqide" target + +$ sudo apt-get install liblablgtksourceview2-ocaml-dev \ + libgtk2.0-dev libgtksourceview2.0-dev +$ opam install lablgtk +``` + +## Building `coqtop` +The general workflow is to first setup a development environment with +the correct `configure` settings, then hacking on Coq, make-ing, and testing. + + +This document will use `$JOBS` to refer to the number of parallel jobs one +is willing to have with `make`. + + +``` +$ git clone git clone https://github.com/coq/coq.git +$ cd coq +$ ./configure -profile devel +$ make -j $JOBS # Make once for `merlin`(autocompletion tool) + +<hack> + +$ make -j $JOBS states # builds just enough to run coqtop +$ bin/coqtop -compile <test_file_name.v> +<goto hack until stuff works> + +<run test-suite> +``` + +To learn how to run the test suite, you can read +[`test-suite/README.md`](../../test-suite/README.md). + +## Coq functions of interest +- `Coqtop.start`: This function is the main entry point of coqtop. +- `Coqtop.parse_args `: This function is responsible for parsing command-line arguments. +- `Coqloop.loop`: This function implements the read-eval-print loop. +- `Vernacentries.interp`: This function is called to execute the Vernacular command user have typed. + It dispatches the control to specific functions handling different Vernacular command. +- `Vernacentries.vernac_check_may_eval`: This function handles the `Check ...` command. + + +## Development environment + tooling +- [`Merlin`](https://github.com/ocaml/merlin) for autocomplete. +- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup) + +## A note about rlwrap + +When using `rlwrap coqtop` make sure the version of `rlwrap` is at least +`0.42`, otherwise you will get + +``` +rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory +``` + +If this happens either update or use an alternate readline wrapper like `ledit`. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f3fc126f92..1eea2443fe 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a @@ -72,11 +82,119 @@ Vernacular commands `tactics/`. In all cases adapting is a matter of changing the module name. +Primitive number parsers + +- For better modularity, the primitive parsers for positive, N and Z + have been split over three files (plugins/syntax/positive_syntax.ml, + plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). + +Parsing + +- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules + Pcoq.Entry and Pcoq.Parsable were introduced to replace it. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq code base. Those unit tests create a dependency on the OUnit test framework. +### Transitioning away from Camlp5 + +In an effort to reduce dependency on camlp5, the use of several grammar macros +is discouraged. Coq is now shipped with its own preprocessor, called coqpp, +which serves the same purpose as camlp5. + +To perform the transition to coqpp macros, one first needs to change the +extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are +handled yet. + +Due to parsing constraints, the syntax of the macros is slightly different, but +updating the source code is mostly a matter of straightforward +search-and-replace. The main differences are summarized below. + +#### OCaml code + +Every piece of toplevel OCaml code needs to be wrapped into braces. + +For instance, code of the form +``` +let myval = 0 +``` +should be turned into +``` +{ +let myval = 0 +} +``` + +#### TACTIC EXTEND + +Steps to perform: +- replace the brackets enclosing OCaml code in actions with braces +- if not there yet, add a leading `|̀ to the first rule + +For instance, code of the form: +``` +TACTIC EXTEND my_tac + [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ] +| [ "tac2" tactic(t) ] -> [ mytac2 t ] +END +``` +should be turned into +``` +TACTIC EXTEND my_tac +| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t } +| [ "tac2" tactic(t) ] -> { mytac2 t } +END +``` + +#### VERNAC EXTEND + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### GEXTEND + +Most plugin writers do not need this low-level interface, but for the sake of +completeness we document it. + +Steps to perform are: +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code in actions into braces { } + +For instance, code of the form +``` +GEXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> do_something x y + | "("; z = LIST0 my_entry; ")" -> do_other_thing z +] ]; +END +``` +should be turned into +``` +GRAMMAR EXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> { do_something x y } + | "("; z = LIST0 my_entry; ")" -> { do_other_thing z } +] ]; +END +``` + +Caveats: +- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases + this as a shorthand for all global entries. Solution: always define a `GLOBAL` + section. +- No complex patterns allowed in token naming. Solution: match on it inside the + OCaml quotation. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt deleted file mode 100644 index c48c2d5d16..0000000000 --- a/dev/doc/setup.txt +++ /dev/null @@ -1,269 +0,0 @@ -This document provides detailed guidance on how to: -- compile Coq -- take advantage of Merlin in Emacs -- enable auto-completion for Ocaml source-code -- use ocamldebug in Emacs for debugging coqtop -The instructions were tested with Debian 8.3 (Jessie). - -The procedure is somewhat tedious, but the final results are (still) worth the effort. - -How to compile Coq ------------------- - -Getting build dependencies: - - sudo apt-get install make opam git - opam init --comp 4.02.3 - # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. - - source ~/.bashrc - - # needed if you want to build "coqtop" target - opam install camlp5 - - # needed if you want to build "coqide" target - sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev - opam install lablgtk - - # needed if you want to build "doc" target - sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \ - hevea texlive-latex-extra latex-xcolor - -Cloning Coq: - - # Go to the directory where you want to clone Coq's source-code. E.g.: - cd ~/git - - git clone https://github.com/coq/coq.git - -Building coqtop: - - cd ~/git/coq - git checkout trunk - make distclean - ./configure -profile devel - make clean - make -j4 coqide printers - -The "-profile devel" enables all options recommended for developers (like -warnings, support for Merlin, etc). Moreover Coq is configured so that -it can be run without installing it (i.e. from the current directory). - -Once the compilation is over check if -- bin/coqtop -- bin/coqide -behave as expected. - - -A note about rlwrap -------------------- - -When using "rlwrap coqtop" make sure the version of rlwrap is at least -0.42, otherwise you will get - - rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory - -If this happens either update or use an alternate readline wrapper like "ledit". - - -How to install and configure Merlin (for Emacs) ------------------------------------------------ - - sudo apt-get install emacs - - opam install tuareg - # Follow the advice displayed at the end as how to update your ~/.emacs file. - - opam install merlin - # Follow the advice displayed at the end as how to update your ~/.emacs file. - -Then add this: - - (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el - (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH - (autoload 'merlin-mode "merlin" "Merlin mode" t) - (add-hook 'tuareg-mode-hook 'merlin-mode) - (add-hook 'caml-mode-hook 'merlin-mode) - (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file") - - ;; Do not use TABs. These confuse Merlin. - (setq-default indent-tabs-mode nil) - -to your ~/.emacs file. - -Further Emacs configuration when we start it for the first time. - -Try to open some *.ml file in Emacs, e.g.: - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Emacs display the following strange message: - - The local variables list in ~/git/coq - contains values that may be safe (*). - - Do you want to apply it? - -Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe." - -Emacs then shows two windows: -- one window that shows the contents of the "toplevel/coqtop.ml" file -- and the other window that shows greetings for new Emacs users. - -If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen." - -The default key-bindings are described here: - - https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch - -If you want, you can customize them by replacing the following lines: - - (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next) - (define-key merlin-map (kbd "C-c C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing) - -in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want. -In the text below we assume that you changed the origin key-bindings in the following way: - - (define-key merlin-map (kbd "C-n") 'merlin-error-next) - (define-key merlin-map (kbd "C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-b") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing) - -Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window. -If you prefer to jump to the definition within the same window, do this: - - <Alt+X> customize-group <ENTER> merlin <ENTER> - - Merlin Locate In New Window - - Value Menu - - Never Open In New Window - - State - - Set For Future Sessions - -Testing (Merlin): - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Go to the end of the file where you will see the "start" function. - -Go to a line where "init_toplevel" function is called. - -If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>. - -If you want to jump back, type: <Ctrl+B> - -If you want to learn the type of the value at current cursor's position, type: <Ctrl+T> - - -Enabling auto-completion in emacs ---------------------------------- - -In Emacs, type: <Alt+M> list-packages <ENTER> - -In the list that is displayed, click on "company". - -A new window appears where just click on "Install" and then answer "Yes". - -These lines: - - (package-initialize) - (require 'company) - ; Make company aware of merlin - (add-to-list 'company-backends 'merlin-company-backend) - ; Enable company on merlin managed buffers - (add-hook 'merlin-mode-hook 'company-mode) - (global-set-key [C-tab] 'company-complete) - -then need to be added to your "~/.emacs" file. - -Next time when you start emacs and partially type some identifier, -emacs will offer the corresponding completions. -Auto-completion can also be manually invoked by typing <Ctrl+TAB>. -Description of various other shortcuts is here. - - http://company-mode.github.io/ - - -Getting along with ocamldebug ------------------------------ - -The default ocamldebug key-bindings are described here. - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369 - -If you want, you can customize them by putting the following commands: - - (global-set-key (kbd "<f5>") 'ocamldebug-break) - (global-set-key (kbd "<f6>") 'ocamldebug-run) - (global-set-key (kbd "<f7>") 'ocamldebug-next) - (global-set-key (kbd "<f8>") 'ocamldebug-step) - (global-set-key (kbd "<f9>") 'ocamldebug-finish) - (global-set-key (kbd "<f10>") 'ocamldebug-print) - (global-set-key (kbd "<f12>") 'camldebug) - -to your "~/.emacs" file. - -Let us try whether ocamldebug in Emacs works for us. -(If necessary, re-)compile coqtop: - - cd ~/git/coq - make -j4 coqide printers - -open Emacs: - - emacs toplevel/coqtop.ml & - -and type: - - <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER> - -As a result, a new window is open at the bottom where you should see: - - (ocd) - -i.e. an ocamldebug shell. - - 1. Switch to the window that contains the "coqtop.ml" file. - 2. Go to the end of the file. - 3. Find the definition of the "start" function. - 4. Go to the "let" keyword that is at the beginning of the first line. - 5. By pressing <F5> you set a breakpoint to the cursor's position. - 6. By pressing <F6> you start the bin/coqtop process. - 7. Then you can: - - step over function calls: <F7> - - step into function calls: <F8> - - or finish execution of the current function until it returns: <F9>. - -Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell. - -The points at which the execution of Ocaml program can stop are defined here: - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350 - - -Installing printers to ocamldebug ---------------------------------- - -There is a pretty comprehensive set of printers defined for many common data types. -You can load them by switching to the window holding the "ocamldebug" shell and typing: - - (ocd) source "../dev/db" - - -Some of the functions were you might want to set a breakpoint and see what happens next ---------------------------------------------------------------------------------------- - -- Coqtop.start : This function is the main entry point of coqtop. -- Coqtop.parse_args : This function is responsible for parsing command-line arguments. -- Coqloop.loop : This function implements the read-eval-print loop. -- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ - It dispatches the control to specific functions handling different Vernacular command. -- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command. diff --git a/dev/doc/translate.txt b/dev/doc/translate.txt deleted file mode 100644 index 5b372c96c3..0000000000 --- a/dev/doc/translate.txt +++ /dev/null @@ -1,495 +0,0 @@ - - How to use the translator - ========================= - - (temporary version to be included in the official - TeX document describing the translator) - -The translator is a smart, robust and powerful tool to improve the -readibility of your script. The current document describes the -possibilities of the translator. - -In case of problem recompiling the translated files, don't waste time -to modify the translated file by hand, read first the following -document telling on how to modify the original files to get a smooth -uniform safe translation. All 60000 lines of Coq lines on our -user-contributions server have been translated without any change -afterwards, and 0,5 % of the lines of the original files (mainly -notations) had to be modified beforehand to get this result. - -Table of contents ------------------ - -I) Implicit Arguments - 1) Strict Implicit Arguments - 2) Implicit Arguments in standard library - -II) Notations - 1) Translating a V7 notation as it was - 2) Translating a V7 notation which conflicts with the new syntax - a) Associativity conflicts - b) Conflicts with other notations - b1) A notation hides another notation - b2) A notation conflicts with the V8 grammar - b3) My notation is already defined at another level - c) How to use V8only with Distfix ? - d) Can I overload a notation in V8, e.g. use "*" and "+" ? - 3) Using the translator to have simplest notations - 4) Setting the translator to automatically use new notations that - wasn't used in old syntax - 5) Defining a construction and its notation simultaneously - -III) Various pitfalls - 1) New keywords - 2) Old "Case" and "Match" - 3) Change of definition or theorem names - 4) Change of tactic names - ---------------------------------------------------------------------- - -I) Implicit Arguments - ------------------ - -1) Strict Implicit Arguments - - "Set Implicit Arguments" changes its meaning in V8: the default is -to turn implicit only the arguments that are _strictly_ implicit (or -rigid), i.e. that remains inferable whatever the other arguments -are. E.g "x" inferable from "P x" is not strictly inferable since it -can disappears if "P" is instanciated by a term which erase "x". - - To respect the old semantics, the default behaviour of the -translator is to replace each occurrence "Set Implicit Arguments" by - - Set Implicit Arguments. - Unset Strict Implicits. - - However, you may wish to adopt the new semantics of "Set Implicit -Arguments" (for instance because you think that the choice of -arguments it setsimplicit is more "natural" for you). In this case, -add the option -strict-implicit to the translator. - - Warning: Changing the number of implicit arguments can break the -notations. Then use the V8only modifier of Notations. - -2) Implicit Arguments in standard library - - Main definitions of standard library have now implicit -arguments. These arguments are dropped in the translated files. This -can exceptionally be a source of incompatibilities which has to be -solved by hand (it typically happens for polymorphic functions applied -to "nil" or "None"). - -II) Notations - --------- - - Grammar (on constr) and Syntax are no longer supported. Replace them by -Notation before translation. - - Precedence levels are now from 0 to 200. In V8, the precedence and -associativity of an operator cannot be redefined. Typical level are -(refer to the chapter on notations in the Reference Manual for the -full list): - - <-> : 95 (no associativity) - -> : 90 (right associativity) - \/ : 85 (right associativity) - /\ : 80 (right associativity) - ~ : 75 (right associativity) - =, <, >, <=, >=, <> : 70 (no associativity) - +, - : 50 (left associativity) - *, / : 40 (left associativity) - ^ : 30 (right associativity) - -1) Translating a V7 notation as it was - - By default, the translator keeps the associativity given in V7 while -the levels are mapped according to the following table: - - the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10] - are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100] - with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L] - - If this is OK for you, just simply apply the translator. - -2) Translating a V7 notation which conflicts with the new syntax - -a) Associativity conflict - - Since the associativity of the levels obtained by translating a V7 -level (as shown on table above) cannot be changed, you have to choose -another level with a compatible associativity. - - You can choose any level between 0 and 200, knowing that the -standard operators are already set at the levels shown on the list -above. - -Example 1: Assume you have a notation - -Infix NONA 2 "=_S" my_setoid_eq. - -By default, the translator moves it to level 30 which is right -associative, hence a conflict with the expected no associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity). - -The translator now knows that it has to translate "=_S" at level 70 -with no associativity. - -Rem: 70 is the "natural" level for relations, hence the choice of 70 -here, but any other level accepting a no-associativity would have been -OK. - -Example 2: Assume you have a notation - -Infix RIGHTA 1 "o" my_comp. - -By default, the translator moves it to level 20 which is left -associative, hence a conflict with the expected right associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity). - -The translator now knows that it has to translate "o" at level 20 -which has the correct "right associativity". - -Rem: We assumed here that the user wants a strong precedence for -composition, in such a way, say, that "f o g + h" is parsed as -"(f o g) + h". To get "o" binding less than the arithmetical operators, -an appropriated level would have been close of 70, and below, e.g. 65. - -b) Conflicts with other notations - -Since the new syntax comes with new keywords and new predefined -symbols, new conflicts can occur. Again, you can use the option V8only -to inform the translator of the new syntax to use. - -b1) A notation hides another notation - -Rem: use Print Grammar constr in V8 to diagnose the overlap and see the -section on factorization in the chapter on notations of the Reference -Manual for hints on how to factorize. - -Example: - -Notation "{ x }" := (my_embedding x) (at level 1). - -overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at -level 99. The conflicts can be solved by left-factorizing the notation -as follows: - -Notation "{ x }" := (my_embedding x) (at level 1) - V8only (at level 0, x at level 99). - -b2) A notation conflicts with the V8 grammar. - -Again, use the V8only modifier to tell the translator to automatically -take in charge the new syntax. - -Example: - -Infix 3 "@" app. - -Since "@" is used in the new syntax for deactivating the implicit -arguments, another symbol has to be used, e.g. "@@". This is done via -the V8only option as follows: - -Infix 3 "@" app V8only "@@" (at level 40, left associativity). - -or, alternatively by - -Notation "x @ y" := (app x y) (at level 3, left associativity) - V8only "x @@ y" (at level 40, left associativity). - -b3) My notation is already defined at another level (or with another -associativity) - -In V8, the level and associativity of a given notation can no longer -be changed. Then, either you adopt the standard reserved levels and -associativity for this notation (as given on the list above) or you -change your notation. - -- To change the notation, follow the directions in section b2. - -- To adopt the standard level, just use V8only without any argument. - -Example. - -Infix 6 "*" my_mult. - -is not accepted as such in V8. Write - -Infix 6 "*" my_mult V8only. - -to tell the translator to use "*" at the reserved level (i.e. 40 with -left associativity). Even better, use interpretation scopes (look at -the Reference Manual). - -c) How to use V8only with Distfix ? - -You can't, use Notation instead of Distfix. - -d) Can I overload a notation in V8, e.g. use "*" and "+" for my own -algebraic operations ? - -Yes, using interpretation scopes (see the corresponding chapter in the -Reference Manual). - -3) Using the translator to have simplest notations - -Thanks to the new syntax, * has now the expected left associativity, -and the symbols <, >, <= and >= are now available. - -Thanks to the interpretation scopes, you can overload the -interpretation of these operators with the default interpretation -provided in Coq. - -This may be a motivation to use the translator to automatically change -the notations while switching to the new syntax. - -See sections b) and d) above for examples. - -4) Setting the translator to automatically use new notations that -wasn't used in old syntax - -Thanks to the "Notation" mechanism, defining symbolic notations is -simpler than in the previous versions of Coq. - -Thanks to the new syntax and interpretation scopes, new symbols and -overloading is available. - -This may be a motivation for using the translator to automatically change -the notations while switching to the new syntax. - -Use for that the commands V8Notation and V8Infix. - -Examples: - -V8Infix "==>" my_relation (at level 65, right associativity). - -tells the translator to write an infix "==>" instead of my_relation in -the translated files. - -V8Infix ">=" my_ge. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files and that the level and associativity are the standard -one (as defined in the chart above). - -V8Infix ">=" my_ge : my_scope. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files, that the level and associativity are the standard -one (as defined in the chart above), but only if scope my_scope is -open or if a delimiting key is available for "my_scope" (see the -Reference Manual). - -5) Defining a construction and its notation simultaneously - -This is permitted by the new syntax. Look at the Reference Manual for -explanation. The translator is not fully able to take this in charge... - -III) Various pitfalls - ---------------- - -1) New keywords - - The following identifiers are new keywords - - "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then"; - "else"; "return"; "mod"; "at"; "let"; "_"; ".(" - - The translator automatically add a "_" to names clashing with a -keyword, except for files. Hence users may need to rename the files -whose name clashes with a keyword. - - Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type" - were already keywords - -2) Old "Case" and "Match" - - "Case" and "Match" are normally automatically translated into - "match" or "match" and "fix", but sometimes it fails to do so. It - typically fails when the Case or Match is argument of a tactic whose - typing context is unknown because of a preceding Intro/Intros, as e.g. in - - Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - - The solution is then to replace the invocation of the sequence of - tactics into several invocation of the elementary tactics as follows - - Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - ^^^ - -3) Change of definition or theorem names - - Type "entier" from fast_integer.v is renamed into "N" by the -translator. As a consequence, user-defined objects of same name "N" -are systematically qualified even tough it may not be necessary. The -same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST -TO GIVE]. - -4) Change of tactics names - - Since tactics names are now lowercase, this can clash with -user-defined tactic definitions. To pally this, clashing names are -renamed by adding an extra "_" to their name. - -====================================================================== -Main examples for new syntax ----------------------------- - -1) Constructions - - Applicative terms don't any longer require to be surrounded by parentheses as -e.g in - - "x = f y -> S x = S (f y)" - - - Product is written - - "forall x y : T, U" - "forall x y, U" - "forall (x y : T) z (v w : V), U" - etc. - - Abstraction is written - - "fun x y : T, U" - "fun x y, U" - "fun (x y : T) z (v w : V), U" - etc. - - Pattern-matching is written - - "match x with c1 x1 x2 => t | c2 y as z => u end" - "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end" - "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with - c1 x1 x2, _ => t | c2 y, d z => u end" - - The last example is the new form of what was written - - "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of - (c1 x1 x2) _ => t | (c2 y) (d z) => u end" - - Pattern-matching of type with one constructors and no dependencies -of the arguments in the resulting type can be written - - "let (x,y,z) as u return P u := t in v" - - Local fixpoints are written - - "fix f (n m:nat) z (x : X) {struct m} : nat := ... - with ..." - - and "struct" tells which argument is structurally decreasing. - - Explicitation of implicit arguments is written - - "f @1:=u v @3:=w t" - "@f u v w t" - -2) Tactics - - The main change is that tactics names are now lowercase. Besides -this, the following renaming are applied: - - "NewDestruct" -> "destruct" - "NewInduction" -> "induction" - "Induction" -> "simple induction" - "Destruct" -> "simple destruct" - - For tactics with occurrences, the occurrences now comes after and - repeated use is separated by comma as in - - "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4" - "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4" - "Simpl 1 3 e" -> "simpl e at 1 3" - -3) Tactic language - - Definitions are now introduced with keyword "Ltac" (instead of -"Tactic"/"Meta" "Definition") and are implicitly recursive -("Recursive" is no longer used). - - The new rule for distinguishing terms from ltac expressions is: - - Write "ltac:" in front of any tactic in argument position and - "constr:" in front of any construction in head position - -4) Vernacular language - -a) Assumptions - - The syntax for commands is mainly unchanged. Declaration of -assumptions is now done as follows - - Variable m : t. - Variables m n p : t. - Variables (m n : t) (u v : s) (w : r). - -b) Definitions - - Definitions are done as follows - - Definition f m n : t := ... . - Definition f m n := ... . - Definition f m n := ... : t. - Definition f (m n : u) : t := ... . - Definition f (m n : u) := ... : t. - Definition f (m n : u) := ... . - Definition f a b (p q : v) r s (m n : t) : t := ... . - Definition f a b (p q : v) r s (m n : t) := ... . - Definition f a b (p q : v) r s (m n : t) := ... : t. - -c) Fixpoints - - Fixpoints are done this way - - Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... . - Fixpoint f x : v := ... . - Fixpoint f (x : t) : v := ... . - - It is possible to give a concrete notation to a fixpoint as follows - - Fixpoint plus (n m:nat) {struct n} : nat as "n + m" := - match n with - | O => m - | S p => S (p + m) - end. - -d) Inductive types - - The syntax for inductive types is as follows - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 (x y : t) : w1 | c2 (z : r) : w2 | ... . - - As seen in the last example, arguments of the constructors can be -given before the colon. If the type itself is omitted (allowed only in -case the inductive type has no real arguments), this yields an -ML-style notation as follows - - Inductive nat : Set := O | S (n:nat). - Inductive bool : Set := true | false. - - It is even possible to define a syntax at the same time, as follows: - - Inductive or (A B:Prop) : Prop as "A \/ B":= - | or_introl (a:A) : A \/ B - | or_intror (b:B) : A \/ B. - - Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B). - diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 3867d4af90..8f9c3171da 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl Coq V8.7 beta 2 & released 6 October 2017 & \\ -Coq V8.7 & released 18 October 2016 & \\ +Coq V8.7.0 & released 18 October 2017 & \\ + +Coq V8.7.1 & released 15 December 2017 & \\ + +Coq V8.7.2 & released 17 February 2018 & \\ + +Coq V8.8 beta1 & released 19 March 2018 & \\ + +Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ +&& \feature{effort towards better documented, better structured ML API}\\ +&& \feature{miscellaneous changes/improvements of existing features}\\ \end{tabular} diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b35571e9ca..48671c03b6 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -10,9 +10,9 @@ versions of Proof General. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). -OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). +OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). -Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). +Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). * [Commands](#commands) - [About](#command-about) diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 2bec09de2b..bccd3fefb4 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -33,7 +33,7 @@ if [ -z "$GUESS_CHECKER" ]; then -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ + -I $COQTOP/plugins/firstorder \ -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 5205350a61..9864fd4d69 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,11 +1,34 @@ #!/usr/bin/env bash -# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging] - set -e -PRNUM=$1 -OPTION=$2 +if [[ $# == 0 ]]; then + echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum" + exit 1 +fi + +while [[ $# -gt 0 ]]; do + case "$1" in + --no-conflict) + NO_CONFLICTS="true" + shift + ;; + --no-signature-check) + NO_SIGNATURE_CHECK="true" + shift + ;; + --stop-before-merging) + STOP_BEFORE_MERGING="true" + shift + ;; + *) + if [[ "$PRNUM" != "" ]]; then + echo "PRNUM was already set to $PRNUM and is now being overridden with $1." + fi + PRNUM="$1" + shift + esac +done if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." @@ -14,7 +37,7 @@ fi SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?") git log master --grep "Merge PR #${PRNUM}" --format="%GG" -if [[ "${SIGNATURE_STATUS}" != "G" ]]; then +if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then echo read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r echo @@ -30,6 +53,14 @@ MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merg if git checkout -b "${BRANCH}"; then if ! git cherry-pick -x "${RANGE}"; then + if [[ "$NO_CONFLICTS" == "true" ]]; then + git status + echo "Conflicts! Aborting..." + git cherry-pick --abort + git checkout - + git branch -d "$BRANCH" + exit 1 + fi echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -59,7 +90,7 @@ if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then fi fi -if [[ "${OPTION}" == "--stop-before-merging" ]]; then +if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then exit 0 fi diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh index f7e05b51cd..33a9ff058e 100755 --- a/dev/tools/check-overlays.sh +++ b/dev/tools/check-overlays.sh @@ -1,8 +1,8 @@ #!/usr/bin/env bash -for f in dev/ci/user-overlays/* +for f in $(git ls-files "dev/ci/user-overlays/") do - if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]]) + if ! ([[ "$f" = dev/ci/user-overlays/README.md ]] || [[ "$f" == *.sh ]]) then >&2 echo "Bad overlay '$f'." >&2 echo "User overlays need to have extension .sh to be picked up!" diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 70a9756e51..ec72f96509 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq"))) + (let ((dir (locate-dominating-file default-directory "META.coq.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c8385da618..98190b05b5 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -17,7 +17,7 @@ let ppripos (ri,pos) = | Reloc_getglobal kn -> print_string ("getglob "^(Constant.to_string kn)^"\n") | Reloc_proj_name p -> - print_string ("proj "^(Constant.to_string p)^"\n") + print_string ("proj "^(Projection.Repr.to_string p)^"\n") ); print_flush () |