diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | dev/ci/README.md | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-crypto-legacy.sh | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 4 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 29 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh | 11 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh | 9 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 83 | ||||
| -rwxr-xr-x | dev/tools/make_git_revision.sh | 11 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 25 |
15 files changed, 127 insertions, 71 deletions
diff --git a/dev/base_include b/dev/base_include index 6f54ecb241..67a7e87d78 100644 --- a/dev/base_include +++ b/dev/base_include @@ -99,7 +99,6 @@ open Evarutil open Evarsolve open Tacred open Evd -open Universes open Termops open Namegen open Indrec diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 5f07aa8fca..b8bea755e0 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1374,7 +1374,7 @@ function copy_coq_license { # FIXME: this is not the micromega license # It only applies to code that was copied into one single file! install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" - install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" + install -D CHANGES.md "$PREFIXCOQ/license_readme/coq/Changes.md" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true fi diff --git a/dev/ci/README.md b/dev/ci/README.md index 24952eb5b7..7853866f62 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project: developer who merges the PR on Coq. There are plans to improve this, cf. [#6724](https://github.com/coq/coq/issues/6724). -Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. Advanced GitLab CI information ------------------------------ @@ -175,6 +175,11 @@ If your repository has access to runners tagged `windows`, setting the secret variable `WINDOWS` to `enabled` will add jobs building Windows versions of Coq (32bit and 64bit). +If the secret variable `WINDOWS` is set to `enabled_all_addons`, +an extended set of addons will be added to the Windows installer. +This leads to a considerable runtime in CI so this is not enabled +by default for pipelines for pull requests. + The Windows jobs are enabled on Coq's repository, where pipelines for pull requests run. diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 1b1aeafa0d..511eaaba9c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -49,11 +49,12 @@ ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_REF:=master}" + +# NB: stdpp and Iris refs are gotten from the opam files in the Iris +# and lambdaRust repos respectively. : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_REF:=master}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index e0395754e5..6bf3138346 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -10,4 +10,5 @@ fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-d 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 && \ + ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 6960a8b98a..95f143bb95 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -9,13 +9,13 @@ install_ssreflect git_download lambdaRust # Extract required version of Iris -Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris git_download Iris # Extract required version of std++ -stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index fcfa591ce1..f257c62dd3 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-25-V1" +# CACHEKEY: "bionic_coq-V2018-10-04-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.01" \ +ENV CAMLP5_VER="7.03" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" # base switch diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index deda42e2b7..918d289ae2 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -37,8 +37,21 @@ SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% SET COQREGTESTING=Y
SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+IF "%WINDOWS%" == "enabled_all_addons" (
+ SET EXTRA_ADDONS=^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot
+ REM addons with build issues
+ REM -addon=vst ^
+ REM -addon=aactactics ^
+) ELSE (
+ SET "EXTRA_ADDONS= "
+)
call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
@@ -47,20 +60,10 @@ call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ -addon=equations ^
-addon=ltac2 ^
-addon=mtac2 ^
- -addon=mathcomp ^
- -addon=menhir ^
- -addon=menhirlib ^
- -addon=compcert ^
- -addon=extlib ^
- -addon=quickchick ^
- -addon=coquelicot ^
+ %EXTRA_ADDONS% ^
-make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-REM addons with build issues
-REM -addon=vst ^
-REM -addon=aactactics ^
-
ECHO "Start Artifact Creation"
TIME /T
diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh new file mode 100644 index 0000000000..484ad8f9e6 --- /dev/null +++ b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh @@ -0,0 +1,11 @@ +if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then + + ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env + ltac2_CI_REF=master+fix-pr8554-change-takes-env + ltac2_CI_GITURL=https://github.com/herbelin/ltac2 + + Equations_CI_BRANCH=master+fix-pr8554-change-takes-env + Equations_CI_REF=master+fix-pr8554-change-takes-env + Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh new file mode 100644 index 0000000000..41c2ad6fef --- /dev/null +++ b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then + + ltac2_CI_REF=rm-section-path + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + Equations_CI_REF=rm-section-path + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index c0cd9c8cdd..000f21c254 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -54,7 +54,7 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. If overlays are missing, ask the author to prepare them and label the PR with the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. @@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push to `master` directly. Don't use the GitHub interface to fix these conflicts. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index fdeb0abed4..7e64f80ac5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,10 +2,22 @@ ### ML API -Termops: +General deprecation -- Internal printing functions have been placed under the - `Termops.Internal` namespace. +- All functions marked [@@ocaml.deprecated] in 8.8 have been + removed. Please, make sure your plugin is warning-free in 8.8 before + trying to port it over 8.9. + +Names + +- Kernel names no longer contain a section path. They now have only two + components (module path and label), which led to some changes in the API: + + KerName.make takes only 2 components + KerName.repr returns only 2 components + KerName.make2 is now KerName.make + Constant.make3 has been removed, use Constant.make2 + Constant.repr3 has been removed, use Constant.repr2 ## Changes between Coq 8.8 and Coq 8.9 @@ -16,8 +28,8 @@ Names - In `Libnames`, the type `reference` and its two constructors `Qualid` and `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be - replaced by a test using `qualid_is_ident`. Extracting the ident part of a - qualid can be done using `qualid_basename`. + replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a + `qualid` can be done using `qualid_basename`. Misctypes @@ -51,20 +63,20 @@ Proof engine ML Libraries used by Coq -- Introduction of a "Smart" module for collecting "smart*" functions, e.g. - Array.Smart.map. -- Uniformization of some names, e.g. Array.Smart.fold_left_map instead - of Array.smartfoldmap. +- Introduction of a `Smart` module for collecting `smart*` functions, e.g. + `Array.Smart.map`. +- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead + of `Array.smartfoldmap`. Printer.ml API -- The mechanism in Printer that allowed dynamically overriding pr_subgoals, - pr_subgoal and pr_goal was removed to simplify the code. It was - earlierly used by PCoq. +- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`, + `pr_subgoal` and `pr_goal` was removed to simplify the code. It was + earlier used by PCoq. Kernel - The following renamings happened: +- 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` @@ -93,19 +105,24 @@ Vernacular commands 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). +- 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. +- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules + `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it. + +Termops + +- Internal printing functions have been placed under the + `Termops.Internal` namespace. ### 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. +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 @@ -140,7 +157,7 @@ let myval = 0 Steps to perform: - replace the brackets enclosing OCaml code in actions with braces -- if not there yet, add a leading `|̀ to the first rule +- if not there yet, add a leading `|` to the first rule For instance, code of the form: ``` @@ -171,8 +188,8 @@ 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 { } +- replace `GEXTEND` with `GRAMMAR EXTEND` +- wrap every occurrence of OCaml code in actions into braces `{ }` For instance, code of the form ``` @@ -222,7 +239,7 @@ All the other bugs kept their number. General deprecation -- All functions marked [@@ocaml.deprecated] in 8.7 have been +- All functions marked `[@@ocaml.deprecated]` in 8.7 have been removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. @@ -250,8 +267,8 @@ We changed the type of the following functions: - `Global.body_of_constant`: same as above. -- `Constrinterp.*` generally, many functions that used to take an - `evar_map ref` have been now switched to functions that will work in +- `Constrinterp.*`: generally, many functions that used to take an + `evar_map ref` have now been switched to functions that will work in a functional way. The old style of passing `evar_map`s as references is not supported anymore. @@ -269,16 +286,16 @@ We have changed the representation of the following types: Some tactics and related functions now support static configurability, e.g.: -- injectable, dEq, etc. takes an argument ~keep_proofs which, - - if None, tells to behave as told with the flag Keep Proof Equalities - - if Some b, tells to keep proof equalities iff b is true +- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which, + - if `None`, tells to behave as told with the flag `Keep Proof Equalities` + - if `Some b`, tells to keep proof equalities iff `b` is true Declaration of printers for arguments used only in vernac command -- It should now use "declare_extra_vernac_genarg_pprule" rather than - "declare_extra_genarg_pprule", otherwise, a failure at runtime might +- It should now use `declare_extra_vernac_genarg_pprule` rather than + `declare_extra_genarg_pprule`, otherwise, a failure at runtime might happen. An alternative is to register the corresponding argument as - a value, using "Geninterp.register_val0 wit None". + a value, using `Geninterp.register_val0 wit None`. Types Alias deprecation and type relocation. @@ -321,7 +338,7 @@ functions when some given constants are traversed: * `declare_reduction_effect`: to declare a hook to be applied when some constant are visited during the execution of some reduction functions - (primarily cbv). + (primarily `cbv`). * `set_reduction_effect`: to declare a constant on which a given effect hook should be called. diff --git a/dev/tools/make_git_revision.sh b/dev/tools/make_git_revision.sh new file mode 100755 index 0000000000..84982f89b9 --- /dev/null +++ b/dev/tools/make_git_revision.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +if [ -x `which git` ] && [ -d .git ] || git rev-parse --git-dir > /dev/null 2>&1 +then + export LANG=C + GIT_BRANCH=$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p') + GIT_HOST=$(hostname) + GIT_PATH=$(pwd) + echo "${GIT_HOST}:${GIT_PATH},${GIT_BRANCH}" + echo $(git log -1 --pretty='format:%H') +fi diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 7c8b9f025c..14094553a2 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -17,7 +17,7 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') -BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v') +BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e15fd776b2..8129a4a867 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -552,23 +552,22 @@ open Libnames let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] - | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ - DirPath.repr dir) in + | Some mp -> DirPath.repr (dirpath_of_string (ModPath.to_string mp)) + in make_qualid ?loc (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = Constant.repr3 cst in - encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) + let (mp,id) = Constant.repr2 cst in + encode_path ?loc "CST" (Some mp) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = MutInd.repr3 kn in - encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] + let (mp,id) = MutInd.repr2 kn in + encode_path ?loc "IND" (Some mp) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = MutInd.repr3 kn in - encode_path ?loc "CSTR" (Some (mp,dir)) + let (mp,id) = MutInd.repr2 kn in + encode_path ?loc "CSTR" (Some mp) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) | VarRef id -> @@ -576,14 +575,14 @@ let raw_string_of_ref ?loc _ = function let short_string_of_ref ?loc _ = function | VarRef id -> qualid_of_ident ?loc id - | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn))) + | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst)) + | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn)) | IndRef (kn,i) -> - encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] + encode_path ?loc "IND" None [Label.to_id (MutInd.label kn)] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None - [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (MutInd.label kn);Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that |