diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-flocq.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-paramcoq.sh | 3 | ||||
| -rw-r--r-- | dev/ci/user-overlays/13958-gares-recordops-api.sh | 6 | ||||
| -rw-r--r-- | dev/core_dune.dbg | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 38 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 10 | ||||
| -rw-r--r-- | dev/dune | 4 | ||||
| -rw-r--r-- | dev/dune_db_408 | 2 | ||||
| -rw-r--r-- | dev/dune_db_409 | 2 | ||||
| -rw-r--r-- | dev/shim/dune | 2 |
12 files changed, 67 insertions, 17 deletions
diff --git a/dev/base_include b/dev/base_include index 061bf1f3e1..b761924b46 100644 --- a/dev/base_include +++ b/dev/base_include @@ -68,7 +68,7 @@ open Constr_matching open Glob_term open Glob_ops open Coercion -open Recordops +open Structures open Detyping open Reductionops open Evarconv diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 67555da0a2..0093b5fca2 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -139,7 +139,8 @@ project compcert "https://github.com/AbsInt/CompCert" "master" ######################################################################## # VST ######################################################################## -project vst "https://github.com/PrincetonUniversity/VST" "master" +# todo: 2021 03 11: switch back to master once vst merges the compcert3.9 branch +project vst "https://github.com/PrincetonUniversity/VST" "compcert3.9" ######################################################################## # cross-crypto @@ -247,7 +248,7 @@ project reduction_effects "https://github.com/coq-community/reduction-effects" " # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122" +project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20210310" ######################################################################## # aac_tactics diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index cb6c3e6452..01723e5b5c 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,10 @@ ci_dir="$(dirname "$0")" git_download flocq -( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) +( cd "${CI_BUILD_DIR}/flocq" + ( if [ ! -x ./configure ]; then + autoconf + ./configure COQEXTRAFLAGS="-compat 8.13"; + fi ) + ./remake "-j${NJOBS}" + ./remake install ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh index d2e0ee89bf..1b2d6a73a2 100755 --- a/dev/ci/ci-paramcoq.sh +++ b/dev/ci/ci-paramcoq.sh @@ -5,4 +5,7 @@ ci_dir="$(dirname "$0")" git_download paramcoq +# Typically flaky on our worker configuration +# https://gitlab.com/coq/coq/-/jobs/1144081161 +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples) diff --git a/dev/ci/user-overlays/13958-gares-recordops-api.sh b/dev/ci/user-overlays/13958-gares-recordops-api.sh new file mode 100644 index 0000000000..0ec50a1dda --- /dev/null +++ b/dev/ci/user-overlays/13958-gares-recordops-api.sh @@ -0,0 +1,6 @@ +overlay metacoq https://github.com/gares/metacoq recordops-api 13958 +overlay mtac2 https://github.com/gares/Mtac2 recordops-api 13958 +overlay elpi https://github.com/gares/coq-elpi recordops-api 13958 +overlay unicoq https://github.com/gares/unicoq recordops-api 13958 +overlay equations https://github.com/gares/Coq-Equations recordops-api 13958 +overlay hierarchy_builder https://github.com/gares/hierarchy-builder coq-master 13958 diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg index da3022644d..db51dc08b6 100644 --- a/dev/core_dune.dbg +++ b/dev/core_dune.dbg @@ -6,7 +6,7 @@ load_printer clib.cma load_printer dynlink.cma load_printer lib.cma load_printer gramlib.cma -load_printer byterun.cma +load_printer coqrun.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index de3d5a3d15..8ebd6b5073 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,17 +10,23 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -Usually, using the latest version of Dune is recommended, see -`dune-project` for the minimum required version; type `dune build` to -build the base Coq libraries. No call to `./configure` is needed. +Usually, using the latest version of Dune is recommended, see the +first line of the `dune-project` file for the minimum required +version. + +It is strongly recommended that you use the helper targets available +in `Makefile.dune`, `make -f Makefile.dune` will display help. Note +that dune will call configure for you if needed, so no need to call +`./configure` in the regular development workflow. + +`dune build @install` will build all the public Coq artifacts; `dune +build` will build all the targets in the workspace, including tests +and documentations. Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -More helper targets are available in `Makefile.dune`, `make -f -Makefile.dune` will display some help. - Dune places build artifacts in a separate directory `_build`; it will also generate an `.install` file so files can be properly installed by package managers. @@ -84,7 +90,11 @@ builds, please see below. ## Documentation and testing targets -Coq's test-suite can be run with `dune runtest`. +Coq's test-suite can be run with `dune runtest`; given that `dune` +still invokes the test-suite makefile, the environment variable +`NJOBS` will control the value of the `-j` option that is passed to +make; common call `NJOBS=8 dune runtest`. This will be resolved in the +future once the test suite is ported to Dune rules. There is preliminary support to build the API documentation and reference manual in HTML format, use `dune build {@doc,@refman-html}` @@ -229,3 +239,17 @@ useful to Coq, some examples are: implicitly loaded plugins / vo files. See the "Running binaries [coqtop / coqide]" section above as to how to correctly call Coq's binaries. + +## Dune cheat sheet + +- `dune build` build all targets in the current workspace +- `dune build @check` build all ML targets as fast as possible, setup merlin +- `dune utop $dir` open a shell for libraries in `$dir` +- `dune exec -- $file` build and execute binary `$file`, can be in path or be an specific name +- `dune build _build/$context/$foo` build target `$foo$` in `$context`, with build dir layout +- `dune build _build/install/$context/foo` build target `$foo$` in `$context`, with install dir layout + +### packaging: + +- `dune subst` generate metadata for a package to be installed / distributed, necessary for opam +- `dune build -p $pkg` build a package in release mode diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 4452baf513..5c8b8944a7 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -344,6 +344,16 @@ Conversion machines noticeable if activated by chance, since it usually breaks control-flow integrity + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: arbitrary code execution on irreducible PArray.set + introduced: 8.13 + impacted released versions: 8.13.0, 8.13.1 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.2 + found by: Melquiond + GH issue number: #13998 + risk: none, unless using primitive array operations; systematic otherwise + Side-effects component: side-effects @@ -21,8 +21,8 @@ %{lib:coq-core.clib:clib.cma} %{lib:coq-core.lib:lib.cma} %{lib:coq-core.kernel:kernel.cma} - %{lib:coq-core.vm:byterun.cma} - %{lib:coq-core.vm:../../stublibs/dllbyterun_stubs.so} + %{lib:coq-core.vm:coqrun.cma} + %{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so} %{lib:coq-core.library:library.cma} %{lib:coq-core.engine:engine.cma} %{lib:coq-core.pretyping:pretyping.cma} diff --git a/dev/dune_db_408 b/dev/dune_db_408 index bc86020d56..dff9b1e9e6 100644 --- a/dev/dune_db_408 +++ b/dev/dune_db_408 @@ -6,7 +6,7 @@ load_printer clib.cma load_printer dynlink.cma load_printer lib.cma load_printer gramlib.cma -load_printer byterun.cma +load_printer coqrun.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma diff --git a/dev/dune_db_409 b/dev/dune_db_409 index adb1f76872..6c9f701b65 100644 --- a/dev/dune_db_409 +++ b/dev/dune_db_409 @@ -5,7 +5,7 @@ load_printer config.cma load_printer clib.cma load_printer lib.cma load_printer gramlib.cma -load_printer byterun.cma +load_printer coqrun.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma diff --git a/dev/shim/dune b/dev/shim/dune index e4cc7699f0..2c7f9c3fa9 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -26,7 +26,7 @@ (targets coqbyte-prelude) (deps %{bin:coqtop.byte} - %{lib:coq-core.kernel:../../stublibs/dllbyterun_stubs.so} + %{lib:coq-core.kernel:../../stublibs/dllcoqrun_stubs.so} %{project_root}/theories/Init/Prelude.vo) (action (with-stdout-to %{targets} |