diff options
Diffstat (limited to 'dev')
30 files changed, 98 insertions, 112 deletions
diff --git a/dev/base_include b/dev/base_include index f375a867bc..b761924b46 100644 --- a/dev/base_include +++ b/dev/base_include @@ -16,7 +16,6 @@ #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; #install_printer (* projection *) ppproj;; -#install_printer (* cl_index *) ppclindex;; #install_printer (* recarg Rtree.t *) ppwf_paths;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; @@ -69,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/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh deleted file mode 100755 index 2550cbb31c..0000000000 --- a/dev/build/osx/make-macos-dmg.sh +++ /dev/null @@ -1,37 +0,0 @@ -#!/bin/bash - -# Fail on first error -set -e - -# Configuration setup -DMGDIR=$PWD/_dmg -VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) -APP=bin/CoqIDE_${VERSION}.app - -# Install Coq into the .app file -make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop - -# Fill .app file with metadata and other .app specific stuff (like non-system .so) -make PRIVATEBINARIES="$APP" -j 1 -l2 "$APP" VERBOSE=1 - -# Create the dmg bundle -mkdir -p "$DMGDIR" -ln -sf /Applications "$DMGDIR/Applications" -cp -r "$APP" "$DMGDIR" - -mkdir -p _build - -# Temporary countermeasure to hdiutil error 5341 -# head -c9703424 /dev/urandom > $DMGDIR/.padding - -hdi_opts=(-volname "coq-$VERSION-installer-macos" - -srcfolder "$DMGDIR" - -ov # overwrite existing file - -format UDZO - -imagekey "zlib-level=9" - - # needed for backward compat since macOS 10.14 which uses APFS by default - # see discussion in #11803 - -fs hfs+ - ) -hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8bcbd90f0b..0093b5fca2 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -79,8 +79,6 @@ project iris "https://gitlab.mpi-sws.org/iris/iris" "" project autosubst "https://github.com/coq-community/autosubst" "master" -project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master" - project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master" ######################################################################## @@ -141,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 @@ -249,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 @@ -308,3 +307,8 @@ project sf "https://github.com/DeepSpec/sf" "master" # Coqtail ######################################################################## project coqtail "https://github.com/whonore/Coqtail" "master" + +######################################################################## +# Deriving +######################################################################## +project deriving "https://github.com/arthuraa/deriving" "master" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 8d8f78e10c..6d1e6d788a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -138,38 +138,8 @@ make() if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; then # Not submake and parallel make requested - command make --output-sync -j "$NJOBS" "$@" + command make -j "$NJOBS" "$@" else - command make --output-sync "$@" + command make "$@" fi } - -# this installs just the ssreflect library of math-comp -install_ssreflect() -{ - echo 'Installing ssreflect' - - git_download mathcomp - - ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \ - make && \ - make install ) - -} - -# this installs just the ssreflect + algebra library of math-comp -install_ssralg() -{ - echo 'Installing ssralg' - - git_download mathcomp - - ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ - make -C ssreflect && \ - make -C ssreflect install && \ - make -C fingroup && \ - make -C fingroup install && \ - make -C algebra && \ - make -C algebra install ) - -} diff --git a/dev/ci/ci-deriving.sh b/dev/ci/ci-deriving.sh new file mode 100755 index 0000000000..c34fc44f69 --- /dev/null +++ b/dev/ci/ci-deriving.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download deriving + +( cd "${CI_BUILD_DIR}/deriving" && make && make tests && make install ) diff --git a/dev/ci/ci-fcsl_pcm.sh b/dev/ci/ci-fcsl_pcm.sh index cb951630c8..e1248c6627 100755 --- a/dev/ci/ci-fcsl_pcm.sh +++ b/dev/ci/ci-fcsl_pcm.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download fcsl_pcm ( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) 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-geocoq.sh b/dev/ci/ci-geocoq.sh index e4fc983e68..0ad9ac0cbb 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssralg - git_download geocoq ( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh index d29e6f1635..7a72462758 100755 --- a/dev/ci/ci-iris.sh +++ b/dev/ci/ci-iris.sh @@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")" # Setup iris_examples and separate dependencies first git_download autosubst -git_download iris_string_ident git_download iris_examples # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) @@ -31,8 +30,5 @@ git_download stdpp # Build autosubst ( cd "${CI_BUILD_DIR}/autosubst" && make && make install ) -# Build iris-string-ident -( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install ) - # Build Iris examples ( cd "${CI_BUILD_DIR}/iris_examples" && make && make install ) diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh index 08686d7ced..62623f4c39 100755 --- a/dev/ci/ci-quickchick.sh +++ b/dev/ci/ci-quickchick.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download quickchick -( cd "${CI_BUILD_DIR}/quickchick" && make && make install) +( cd "${CI_BUILD_DIR}/quickchick" && make && make install-plugin) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8f14625c63..00729cd168 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc, pytest for coqtail -RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ +RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ pytest==5.4.3 @@ -44,7 +44,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.13.0" + BASE_ONLY_OPAM="elpi.1.13.1" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh new file mode 100644 index 0000000000..9b8d1a63d9 --- /dev/null +++ b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh @@ -0,0 +1 @@ +overlay compcert https://github.com/Lysxia/CompCert no-collision-projection 13852 diff --git a/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh new file mode 100644 index 0000000000..d860cfec01 --- /dev/null +++ b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/pi8027/coq-elpi coq-overlay-13912 13912 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/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh new file mode 100644 index 0000000000..d1606711dc --- /dev/null +++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh @@ -0,0 +1 @@ +overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050 diff --git a/dev/ci/user-overlays/14111-gares-update-elpi.sh b/dev/ci/user-overlays/14111-gares-update-elpi.sh new file mode 100644 index 0000000000..8827127a38 --- /dev/null +++ b/dev/ci/user-overlays/14111-gares-update-elpi.sh @@ -0,0 +1,2 @@ +overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.5 14111 +overlay hierarchy_builder https://github.com/math-comp/hierarchy-builder coq-master+1.1.0 14111 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 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 57c325f698..1697a19668 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -114,6 +114,11 @@ list of contributors between Coq revisions. Typically used with `VX.X+alpha..vX.X` to check the contributors of version `VX.X`. + Note that this script relies on `.mailmap` to merge multiple + identities. If you notice anything incorrect while using it, use + the opportunity to fix the `.mailmap` file. Same thing if you want + to have the full name of a contributor shown instead of a pseudonym. + ## For each release (preview, final, patch-level) ## - [ ] Ensure that there exists a milestone for the following version. @@ -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-dbg.in b/dev/dune-dbg.in index 47dfbad3a0..cc8574c6d6 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -26,4 +26,4 @@ esac emacs="${INSIDE_EMACS:+-emacs}" -ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@" +ocamldebug $emacs $(ocamlfind query -recursive -i-format coq-core.top_printers) -I +threads -I dev $exe "$@" 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/nixpkgs.nix b/dev/nixpkgs.nix index a582a70e0a..37e39a99a9 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/0bbeca2ff952e6a171534793ddd0fa97c8f9546a.tar.gz"; - sha256 = "0h1y4ffvyvkqs6k2pak02pby25va7c6c1y4p8xkwlzqwswxqxvfl"; + url = "https://github.com/NixOS/nixpkgs/archive/5c7a370a208d93d458193fc05ed84ced0ba7f387.tar.gz"; + sha256 = "1jkn71xscsk4rb0agbp5saf06hy36qvy512zzh3881pkkn67i9js"; }) 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} diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh index c968f2e952..0b0d01c7e2 100644..100755 --- a/dev/tools/list-contributors.sh +++ b/dev/tools/list-contributors.sh @@ -1,15 +1,15 @@ #!/usr/bin/env bash # For compat with OSX which has a non-gnu sed which doesn't support -z -SED=`which gsed || which sed` +SED=`(which gsed || which sed) 2> /dev/null` if [ $# != 1 ]; then - error "usage: $0 rev0..rev1" + echo "usage: $0 rev0..rev1" exit 1 fi git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp cat contributors.tmp | wc -l | xargs echo "Contributors:" -cat contributors.tmp | gsed -z "s/\n/, /g" +cat contributors.tmp | $SED -z "s/\n/, /g" echo rm contributors.tmp diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index fe95a59d9b..5d37c60bca 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -12,7 +12,6 @@ install_printer Top_printers.ppmind install_printer Top_printers.ppind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid -install_printer Top_printers.ppclindex install_printer Top_printers.ppscheme install_printer Top_printers.ppwf_paths install_printer Top_printers.ppevar diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f8fd8b3d5b..67fe7b980b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -52,7 +52,6 @@ let ppmind kn = pp(MutInd.debug_print kn) let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) -let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) let prrecarg = Declareops.pp_recarg diff --git a/dev/top_printers.mli b/dev/top_printers.mli index b4b24d743a..ba7d92f907 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,8 +29,6 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Coercionops.cl_index -> unit - val ppscheme : 'a Ind_tables.scheme_kind -> unit val prrecarg : Declarations.recarg -> Pp.t |