aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include6
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh131
-rwxr-xr-xdev/ci/ci-equations.sh3
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile8
-rw-r--r--dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh19
-rw-r--r--dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh6
-rw-r--r--dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh6
-rw-r--r--dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh9
-rw-r--r--dev/doc/INSTALL.make.md258
-rw-r--r--dev/doc/README.md4
-rw-r--r--dev/doc/changes.md10
-rw-r--r--dev/doc/critical-bugs12
-rw-r--r--dev/dune-workspace.all2
-rwxr-xr-xdev/lint-repository.sh3
-rw-r--r--dev/nixpkgs.nix4
-rwxr-xr-xdev/tools/update-compat.py109
-rw-r--r--dev/top_printers.ml2
-rw-r--r--dev/top_printers.mli2
18 files changed, 383 insertions, 211 deletions
diff --git a/dev/base_include b/dev/base_include
index 4841db8953..96a867475d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -60,11 +60,11 @@ open Cases
open Pattern
open Patternops
open Cbv
-open Classops
+open Coercionops
open Arguments_renaming
open Pretyping
open Cbv
-open Classops
+open Coercionops
open Clenv
open Clenvtac
open Constr_matching
@@ -134,7 +134,7 @@ open Tacticals
open Tactics
open Eqschemes
-open Class
+open ComCoercion
open ComDefinition
open Indschemes
open Ind_tables
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 78c0b4b2c7..859b3e3166 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -921,69 +921,6 @@ function make_gtk_sourceview3 {
build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.11 tar.xz make_arch_pkg_config
}
-##### FLEXDLL FLEXLINK #####
-
-# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.)
-# For MinGW it is not even possible to first build an Ocaml without flexlink support,
-# Because Makefile.nt doesn't support this. So we have to use a binary flexlink.
-# One could of cause do a bootstrap run ...
-
-# Install flexdll objects
-
-function install_flexdll {
- cp flexdll.h "$PREFIXMINGW/include"
- if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
- cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
- cp flexdll*_mingw.o "$PREFIXOCAML/bin"
- elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
- cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin"
- cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
- else
- echo "Unknown target architecture"
- return 1
- fi
-}
-
-# Install flexlink
-
-function install_flexlink {
- cp flexlink.exe "/usr/$TARGET_ARCH/bin"
-
- cp flexlink.exe "$PREFIXOCAML/bin"
-}
-
-# Get binary flexdll flexlink for building OCaml
-# An alternative is to first build an OCaml without shared library support and build flexlink with it
-
-function get_flex_dll_link_bin {
- if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then
- install_flexdll
- install_flexlink
- build_post
- fi
-}
-
-# Build flexdll and flexlink from sources after building OCaml
-
-function make_flex_dll_link {
- if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then
- if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
- # shellcheck disable=SC2086
- log1 make $MAKE_OPT build_mingw flexlink.exe
- elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
- # shellcheck disable=SC2086
- log1 make $MAKE_OPT build_mingw64 flexlink.exe
- else
- echo "Unknown target architecture"
- return 1
- fi
- install_flexdll
- install_flexlink
- log2 make clean
- build_post
- fi
-}
-
##### LN replacement #####
# Note: this does support symlinks, but symlinks require special user rights on Windows.
@@ -1016,39 +953,22 @@ function make_arch_pkg_config {
##### OCAML #####
function make_ocaml {
- get_flex_dll_link_bin
- if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then
- # See README.win32.adoc
- cp config/m-nt.h byterun/caml/m.h
- cp config/s-nt.h byterun/caml/s.h
- if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
- cp config/Makefile.mingw config/Makefile
- elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
- cp config/Makefile.mingw64 config/Makefile
- else
- echo "Unknown target architecture"
- return 1
- fi
+ if build_prep https://github.com/ocaml/ocaml/archive 4.08.1 tar.gz 1 ocaml-4.08.1 ; then
+ # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc
- # Prefix is fixed in make file - replace it with the real one
- # TODO: this might not work if PREFIX contains spaces
- sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
+ # get flexdll sources into folder ./flexdll
+ get_expand_source_tar https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 flexdll
# We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
- # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
- # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
- # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
- # So we put an explicit path in there
- sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
-
- # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
- # I verified that 4.02.3 still doesn't support parallel build
- log2 make world -f Makefile.nt
- log2 make bootstrap -f Makefile.nt
- log2 make opt -f Makefile.nt
- log2 make opt.opt -f Makefile.nt
- log2 make install -f Makefile.nt
- # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
+ logn configure ./configure --build=i686-pc-cygwin --host="$TARGET_ARCH" --prefix="$PREFIXOCAML" --libdir="$PREFIXOCAML/libocaml"
+
+ log2 make flexdll $MAKE_OPT
+ # Note the next command might change after 4.09.x to just make
+ # see https://github.com/ocaml/ocaml/blob/4.09/README.win32.adoc
+ # compare to https://github.com/ocaml/ocaml/blob/4.10/README.win32.adoc
+ log2 make world.opt $MAKE_OPT
+ log2 make flexlink.opt $MAKE_OPT
+ log2 make install $MAKE_OPT
# Move license files and other into into special folder
if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
@@ -1065,7 +985,6 @@ function make_ocaml {
build_post
fi
- make_flex_dll_link
}
##### OCAML EXTRA TOOLS #####
@@ -1099,7 +1018,7 @@ function make_num {
function make_ocamlbuild {
make_ocaml
- if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then
+ if build_prep https://github.com/ocaml/ocamlbuild/archive 0.14.0 tar.gz 1 ocamlbuild-0.14.0; then
log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib
log1 make $MAKE_OPT
log2 make install
@@ -1112,6 +1031,7 @@ function make_ocamlbuild {
function make_findlib {
make_ocaml
make_ocamlbuild
+ # Note: latest is 1.8.1 but http://projects.camlcity.org/projects/dl/findlib-1.8.1/doc/README says this is for OCaml 4.09
if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
# Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
@@ -1132,11 +1052,22 @@ function make_findlib {
function make_dune {
make_ocaml
- if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
+ if build_prep https://github.com/ocaml/dune/archive/ 2.0.0 tar.gz 1 dune-2.0.0 ; then
log2 make release
log2 make install
+ # Dune support libs, we don't install glob and action-plugin as
+ # they are not needed by Coq
+ logn dune-private-build dune build -p dune-private-libs @install
+ logn dune-private-install dune install dune-private-libs
+
+ logn dune-configurator-build dune build -p dune-configurator @install
+ logn dune-configurator-install dune install dune-configurator
+
+ logn dune-build-info dune build -p dune-build-info @install
+ logn dune-build-info dune install dune-build-info
+
build_post
fi
}
@@ -1191,7 +1122,8 @@ function make_ocaml_cairo2 {
log2 dune build cairo2.install
log2 dune install cairo2
- log2 dune clean
+ # See https://github.com/ocaml/dune/issues/2921
+ # log2 dune clean
build_post
fi
@@ -1216,7 +1148,8 @@ function make_lablgtk {
log2 dune build -p lablgtk3-sourceview3
log2 dune install lablgtk3-sourceview3
- log2 dune clean
+ # See https://github.com/ocaml/dune/issues/2921
+ # log2 dune clean
build_post
fi
}
@@ -1372,7 +1305,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 INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt"
+ install -D INSTALL.md "$PREFIXCOQ/license_readme/coq/Install.txt"
install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
fi
}
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index b58a794da2..871d033f5b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,5 +5,4 @@ ci_dir="$(dirname "$0")"
git_download equations
-( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \
- make && make test-suite && make examples && make install)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e80f96362b..b8f9d99702 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-11-25-V01"
+# CACHEKEY: "bionic_coq-V2019-12-08-V82"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
# We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
# Basic OPAM setup
ENV NJOBS="2" \
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
# 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.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \
CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
BASE_ONLY_OPAM="elpi.1.8.0"
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
# EDGE switch
ENV COMPILER_EDGE="4.09.0" \
COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
- BASE_OPAM_EDGE="dune-release.1.3.2"
+ BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
# EDGE+flambda switch, we install CI_OPAM as to be able to use
# `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
new file mode 100644
index 0000000000..bb65beb043
--- /dev/null
+++ b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
@@ -0,0 +1,19 @@
+if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then
+
+ elpi_CI_REF=expose-comind-univ
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+ equations_CI_REF=expose-comind-univ
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ paramcoq_CI_REF=expose-comind-univ
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+ mtac2_CI_REF=expose-comind-univ
+ mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+ rewriter_CI_REF=cleanup-comind-univ
+ rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter
+
+
+fi
diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
new file mode 100644
index 0000000000..fb66217487
--- /dev/null
+++ b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then
+
+ quickchick_CI_REF=master+adapt-coq-pr11141
+ quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh
new file mode 100644
index 0000000000..e0d9dc6469
--- /dev/null
+++ b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11172" ] || [ "$CI_BRANCH" = "master+coercion-notation-interleaved-printing" ]; then
+
+ elpi_CI_REF=coq-master+mini-fix-mkGApp
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
new file mode 100644
index 0000000000..a95170a455
--- /dev/null
+++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then
+
+ elpi_CI_REF=rename-class-files
+ elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+ mtac2_CI_REF=rename-class-files
+ mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md
new file mode 100644
index 0000000000..3db5d0b14f
--- /dev/null
+++ b/dev/doc/INSTALL.make.md
@@ -0,0 +1,258 @@
+Quick Installation Procedure using Make.
+----------------------------------------
+
+ $ ./configure
+ $ make
+ $ make install (you may need superuser rights)
+
+Detailed Installation Procedure.
+--------------------------------
+
+1. Check that you have the OCaml compiler installed on your
+ computer and that `ocamlc` (or, better, its native code version
+ `ocamlc.opt`) is in a directory which is present in your $PATH
+ environment variable. At the time of writing this document, all
+ versions of Objective Caml later or equal to 4.05.0 are
+ supported.
+
+ To get Coq in native-code, (which runs 4 to 10 times faster than
+ bytecode, but it takes more time to get compiled and the binary is
+ bigger), you will also need the `ocamlopt` (or its native code version
+ `ocamlopt.opt`) command.
+
+2. The uncompression and un-tarring of the distribution file gave birth
+ to a directory named "coq-8.xx". You can rename this directory and put
+ it wherever you want. Just keep in mind that you will need some spare
+ space during the compilation (reckon on about 300 Mb of disk space
+ for the whole system in native-code compilation). Once installed, the
+ binaries take about 30 Mb, and the library about 200 Mb.
+
+3. First you need to configure the system. It is done automatically with
+ the command:
+
+ ./configure <options>
+
+ The `configure` script will ask you for directories where to put
+ the Coq binaries, standard library, man pages, etc. It will propose
+ default values.
+
+ For a list of options accepted by the `configure` script, run
+ `./configure -help`. The main options accepted are:
+
+ * `-prefix <dir>`
+ Binaries, library, and man pages will be respectively
+ installed in `<dir>/bin`, `<dir>/lib/coq`, and `<dir>/man`
+
+ * `-bindir <dir>` (default: `/usr/local/bin`)
+ Directory where the binaries will be installed
+
+ * `-libdir <dir>` (default: `/usr/local/lib/coq`)
+ Directory where the Coq standard library will be installed
+
+ * `-mandir <dir>` (default: `/usr/local/share/man`)
+ Directory where the Coq manual pages will be installed
+
+ * `-arch <value>` (default is the result of the command `arch`)
+ An arbitrary architecture name for your machine (useful when
+ compiling Coq on two different architectures for which the
+ result of "arch" is the same, e.g. Sun OS and Solaris)
+
+ * `-local`
+ Compile Coq to run in its source directory. The installation (step 6)
+ is not necessary in that case.
+
+ * `-browser <command>`
+ Use <command> to open an URL in a browser. %s must appear in <command>,
+ and will be replaced by the URL.
+
+ * `-flambda-opts <flags>`
+ This experimental option will pass specific user flags to the
+ OCaml optimizing compiler. In most cases, this option is used
+ to tweak the flambda backend; for maximum performance we
+ recommend using:
+
+ -flambda-opts `-O3 -unbox-closures`
+
+ but of course you are free to try with a different combination
+ of flags. You can read more at
+ https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+ There is a known problem with certain OCaml versions and
+ `native_compute`, that will make compilation to require
+ a large amount of RAM (>= 10GiB) in some particular files.
+
+ We recommend disabling native compilation (`-native-compiler no`)
+ with flambda unless you use OCaml >= 4.07.0.
+
+ c.f. https://caml.inria.fr/mantis/view.php?id=7630
+
+ If you want your build to be reproducible, ensure that the
+ SOURCE_DATE_EPOCH environment variable is set as documented in
+ https://reproducible-builds.org/specs/source-date-epoch/
+
+4. Still in the root directory, do
+
+ make
+
+ to compile Coq in the best OCaml mode available (native-code if supported,
+ bytecode otherwise).
+
+ This will compile the entire system. This phase can take more or less time,
+ depending on your architecture and is fairly verbose. On a multi-core machine,
+ it is recommended to compile in parallel, via make -jN where N is your number
+ of cores.
+
+5. You can now install the Coq system. Executables, libraries, and
+ manual pages are copied in some standard places of your system,
+ defined at configuration time (step 3). Just do
+
+ umask 022
+ make install
+
+ Of course, you may need superuser rights to do that.
+
+6. Optionally, you could build the bytecode version of Coq via:
+
+ make byte
+
+ and install it via
+
+ make install-byte
+
+ This version is much slower than the native code version of Coq, but could
+ be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+ toplevel accessible via the Drop command.
+
+7. You can now clean all the sources. (You can even erase them.)
+
+ make clean
+
+Installation Procedure For Plugin Developers.
+---------------------------------------------
+
+If you wish to write plugins you *must* keep the Coq sources, without
+cleaning them. Therefore, to avoid a duplication of binaries and library,
+it is not necessary to do the installation step (6- above). You just have
+to tell it at configuration step (4- above) with the option -local :
+
+ ./configure -local <other options>
+
+Then compile the sources as described in step 5 above. The resulting
+binaries will reside in the subdirectory bin/.
+
+Unless you pass the -nodebug option to ./configure, the -g option of the
+OCaml compiler will be used during compilation to allow debugging.
+See the debugging file in dev/doc and the chapter 15 of the Coq Reference
+Manual for details about how to use the OCaml debugger with Coq.
+
+
+The Available Commands.
+-----------------------
+
+There are two Coq commands:
+
+ coqtop The Coq toplevel
+ coqc The Coq compiler
+
+Under architecture where ocamlopt is available, coqtop is the native code
+version of Coq. On such architecture, you could additionally request
+the build of the bytecode version of Coq via 'make byte' and install it via
+'make install-byte'. This will create an extra binary named coqtop.byte,
+that could be used for debugging purpose. If native code isn't available,
+coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+and coqc selects a particular binary.
+
+* `coqtop` launches Coq in the interactive mode. By default it loads
+ basic logical definitions and tactics from the Init directory.
+
+* `coqc` allows compilation of Coq files directly from the command line.
+ To compile a file foo.v, do:
+
+ coqc foo.v
+
+ It will produce a file `foo.vo`, that you can now load through the Coq
+ command `Require`.
+
+ A detailed description of these commands and of their options is given
+ in the Reference Manual (which you can get in the doc/
+ directory, or read online on http://coq.inria.fr/doc/)
+ and in the corresponding manual pages.
+
+Compiling For Different Architectures.
+--------------------------------------
+
+This section explains how to compile Coq for several architecture, sharing
+the same sources. The important fact is that some files are architecture
+dependent (`.cmx`, `.o` and executable files for instance) but others are not
+(`.cmo` and `.vo`). Consequently, you can :
+
+- save some time during compilation by not cleaning the architecture
+ independent files;
+
+- save some space during installation by sharing the Coq standard
+ library (which is fully architecture independent).
+
+So, in order to compile Coq for a new architecture, proceed as follows:
+
+* Omit step 7 above and clean only the architecture dependent files:
+ it is done automatically with the command
+
+ make archclean
+
+* Configure the system for the new architecture:
+
+ ./configure <options>
+
+ You can specify the same directory for the standard library but you
+ MUST specify a different directory for the binaries (of course).
+
+* Compile and install the system as described in steps 5 and 6 above.
+
+Moving Binaries Or Library.
+---------------------------
+
+If you move both the binaries and the library in a consistent way,
+Coq should be able to still run. Otherwise, Coq may be "lost",
+running "coqtop" would then return an error message of the kind:
+
+ Error during initialization :
+ Error: cannot guess a path for Coq libraries; please use -coqlib option
+
+You can then indicate the new places to Coq, using the options -coqlib :
+
+ coqtop -coqlib <new directory>
+
+See also next section.
+
+Dynamically Loaded Libraries For Bytecode Executables.
+------------------------------------------------------
+
+Some bytecode executables of Coq use the OCaml runtime, which dynamically
+loads a shared library (.so or .dll). When it is not installed properly, you
+can get an error message of this kind:
+
+ Fatal error: cannot load shared library dllcoqrun
+ Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+In this case, you need either:
+
+- to set the `CAML_LD_LIBRARY_PATH` environment variable to point to the
+ directory where dllcoqrun.so is; this is suitable when you want to run
+ the command a limited number of times in a controlled environment (e.g.
+ during compilation of binary packages);
+- install dllcoqrun.so in a location listed in the file ld.conf that is in
+ the directory of the standard library of OCaml;
+- recompile your bytecode executables after reconfiguring the location
+ of the shared library:
+
+ ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
+
+ where `<path>` is the directory where the dllcoqrun.so is installed;
+- (not recommended) compile bytecode executables with a custom OCaml
+ runtime by using:
+
+ ./configure -custom ...
+
+ be aware that stripping executables generated this way, or performing
+ other executable-specific operations, will make them useless.
diff --git a/dev/doc/README.md b/dev/doc/README.md
index bc281e0d94..ba53605b0e 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -43,8 +43,12 @@ To learn how to run the test suite, you can read
## 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)
+- [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) provides
+ support for automatic formatting of OCaml code. To use it please run
+ `dune build @fmt`, see `ocamlformat`'s documentation for more help.
## A note about rlwrap
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d394c3401..04b20c6889 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
## Changes between Coq 8.11 and Coq 8.12
+### ML API
+
+Printers:
+
+- Functions such as Printer.pr_lconstr_goal_style_env have been
+ removed, use instead functions such as pr_lconstr with label
+ `goal_concl_style:true`. Functions such as
+ Constrextern.extern_constr which were taking a boolean argument for
+ the goal style now take instead a label.
+
## Changes between Coq 8.10 and Coq 8.11
### ML API
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..2d187f7bae 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -255,6 +255,18 @@ Conversion machines
GH issue number: #9925
risk:
+ component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+ summary: broken long multiplication primitive integer emulation layer on 32 bits
+ introduced: e43b176
+ impacted released versions: 8.10.0, 8.10.1, 8.10.2
+ impacted development branches: 8.11
+ impacted coqchk versions: none (no virtual machine in coqchk)
+ fixed in: 4e176a7
+ found by: Soegtrop, Melquiond
+ exploit: test-suite/bugs/closed/bug_11321.v
+ GH issue number: #11321
+ risk: critical, as any BigN computation on 32-bit architectures is wrong
+
component: "native" conversion machine (translation to OCaml which compiles to native code)
summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
introduced: V8.5
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 28e8773e25..49e338d0a5 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,4 +1,4 @@
-(lang dune 1.10)
+(lang dune 2.0)
; Add custom flags here. Default developer profile is `dev`
(context (opam (switch 4.05.0)))
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..224601bbce 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
echo Checking overlays
dev/tools/check-overlays.sh || CODE=1
+echo Checking ocamlformat
+dune build @fmt || CODE=1
+
exit $CODE
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index e7a0ba4f6c..677377f868 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
import (fetchTarball {
- url = "https://github.com/NixOS/nixpkgs/archive/4cd2cb43fb3a87f48c1e10bb65aee99d8f24cb9d.tar.gz";
- sha256 = "1d6rmq67kdg5gmk94wx2774qw89nvbhy6g1f2lms3c9ph37hways";
+ url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz";
+ sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq";
})
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 7312c2a5af..ddb0362186 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -15,10 +15,8 @@ from io import open
# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
# with the deleted file.
# - Remove any notations in the standard library which have `compat "U.U"`.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-# bumping all the version numbers by one, and update the interpretations
-# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+# by bumping all the version numbers by one.
#
# - Remove the file
# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
@@ -38,10 +36,8 @@ from io import open
# - Update
# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
# with the added file.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-# bumping all the version numbers by one, and update the interpretations
-# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+# by bumping all the version numbers by one.
# - Update the files
# [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
# [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
@@ -70,10 +66,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
RELEASE_NUMBER_OF_OLD_VERSIONS = 2
MASTER_NUMBER_OF_OLD_VERSIONS = 3
EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli')
-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')
TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
@@ -248,118 +241,38 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
contents = contents.replace(header, '%s\n%s' % (header, line))
update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args)
-def update_compat_versions_type_line(new_versions, contents, relpath):
- compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current'])
- new_compat_line = 'type compat_version = %s' % compat_version_string
- new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE)
- if new_compat_line not in new_contents:
- raise Exception("Could not find 'type compat_version =' in %s" % relpath)
- return new_contents
-
-def update_version_compare(new_versions, contents, relpath):
- first_line = 'let version_compare v1 v2 = match v1, v2 with'
- new_lines = [first_line]
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | %s, %s -> 0' % (V, V))
- new_lines.append(' | %s, _ -> -1' % V)
- new_lines.append(' | _, %s -> 1' % V)
- new_lines.append(' | Current, Current -> 0')
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find version_compare in %s' % relpath)
- return new_contents
-
-def update_pr_version(new_versions, contents, relpath):
- first_line = 'let pr_version = function'
- new_lines = [first_line]
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | %s -> "%s"' % (V, v))
- new_lines.append(' | Current -> "current"')
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find pr_version in %s' % relpath)
- return new_contents
-
-def update_add_compat_require(new_versions, contents, relpath):
- first_line = 'let add_compat_require opts v ='
- new_lines = [first_line, ' match v with']
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext='')))
- new_lines.append(' | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext=''))
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find add_compat_require in %s' % relpath)
- return new_contents
-
-def update_parse_compat_version(new_versions, contents, relpath, **args):
+def update_get_compat_file(new_versions, contents, relpath):
line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current
- first_line = 'let parse_compat_version = let open Flags in function'
+ first_line = 'let get_compat_file = function'
split_contents = contents[contents.index(first_line):].split('\n')
while True:
cur_line = split_contents[:line_count][-1]
if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None:
break
- elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None:
+ elif re.match(r'^ \| "[0-9\.]*" -> "Coq.Compat.Coq[0-9]*"$', cur_line) is not None:
line_count += 1
else:
- raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
+ raise Exception('Could not recognize line %d of get_compat_file in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
old_function_lines = split_contents[:line_count]
all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines))
invalid_versions = tuple(i for i in all_versions if i not in new_versions)
new_function_lines = [first_line]
- for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))):
+ for v, V in reversed(list(zip(new_versions, ['"Coq.Compat.Coq%s%s"' % tuple(v.split('.')) for v in new_versions]))):
new_function_lines.append(' | "%s" -> %s' % (v, V))
new_function_lines.append(' | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions))
new_lines = '\n'.join(new_function_lines)
new_contents = contents.replace('\n'.join(old_function_lines), new_lines)
if new_lines not in new_contents:
- raise Exception('Could not find parse_compat_version in %s' % relpath)
+ raise Exception('Could not find get_compat_file in %s' % relpath)
return new_contents
-def check_no_old_versions(old_versions, new_versions, contents, relpath):
- for v in old_versions:
- if v not in new_versions:
- V = 'V%s_%s' % tuple(v.split('.'))
- if V in contents:
- raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
-
-def update_flags_mli(old_versions, new_versions, **args):
- contents = get_file(FLAGS_MLI_PATH)
- new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
-
-def update_flags_ml(old_versions, new_versions, **args):
- contents = get_file(FLAGS_ML_PATH)
- new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
-
def update_coqargs_ml(old_versions, new_versions, **args):
contents = get_file(COQARGS_ML_PATH)
- new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+ new_contents = update_get_compat_file(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
-def update_g_vernac(old_versions, new_versions, **args):
- contents = get_file(G_VERNAC_PATH)
- new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
-
def update_flags(old_versions, new_versions, **args):
- update_flags_mli(old_versions, new_versions, **args)
- update_flags_ml(old_versions, new_versions, **args)
update_coqargs_ml(old_versions, new_versions, **args)
- update_g_vernac(old_versions, new_versions, **args)
def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args):
assert(len(new_versions) == len(test_suite_paths))
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f7f2bcdcff..835c20a4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -47,7 +47,7 @@ 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(Classops.pr_cl_index cl)
+let ppclindex cl = pp(Coercionops.pr_cl_index cl)
let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
let prrecarg = function
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5a2144f996..133326523b 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit
val ppsp : Libnames.full_path -> unit
val ppqualid : Libnames.qualid -> unit
-val ppclindex : Classops.cl_index -> unit
+val ppclindex : Coercionops.cl_index -> unit
val ppscheme : 'a Ind_tables.scheme_kind -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:47:32 +0000