diff options
Diffstat (limited to 'dev')
28 files changed, 622 insertions, 851 deletions
diff --git a/dev/README b/dev/README index 814f609576..b446c3e974 100644 --- a/dev/README +++ b/dev/README @@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- -Makefile.dir: makefile dedicated to intensive work in a given directory -Makefile.subdir: makefile dedicated to intensive work in a given subdirectory -Makefile.devel: utilities to automatically launch coq in various states -Makefile.common: used by other Makefiles 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 diff --git a/dev/TODO b/dev/TODO deleted file mode 100644 index e62ee6e537..0000000000 --- a/dev/TODO +++ /dev/null @@ -1,22 +0,0 @@ - - o options de la ligne de commande - - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml - - o arguments implicites - - les calculer une fois pour toutes à la déclaration (dans Declare) - et stocker cette information dans le in_variable, in_constant, etc. - - o Environnements compilés (type Environ.compiled_env) - - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) - - o Efficacité - - utiliser DOPL plutôt que DOPN (sauf pour Case) - - batch mode => pas de undo, ni de reset - - conversion : déplier la constante la plus récente - - un cache pour type_of_const, type_of_inductive, type_of_constructor, - lookup_mind_specif - - o Toplevel - - parsing de la ligne de commande : utiliser Arg ??? - - diff --git a/dev/base_include b/dev/base_include index bfbf6bb5d8..79ecd73e0d 100644 --- a/dev/base_include +++ b/dev/base_include @@ -194,8 +194,8 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; +let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of implicit syntax *) diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index b43ada9076..cbe2a5186f 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -4,19 +4,13 @@ set -e # Configuration setup -eval `opam config env` -make distclean OUTDIR=$PWD/_install DMGDIR=$PWD/_dmg -./configure -debug -prefix $OUTDIR -native-compiler no VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app # Create a .app file with CoqIDE -~/.local/bin/jhbuild run make -j -l2 $APP - -# Build Coq and run test-suite -make && make check +make -j $NJOBS -l2 $APP # Add Coq to the .app file make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop @@ -29,7 +23,9 @@ 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 +# head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg +hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index b2efe2ddd4..a420b5d8bb 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -344,6 +344,9 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" ( IF NOT "%CYGWIN_QUIET%" == "Y" ( SET RUNSETUP=Y ) +IF "%COQREGTESTING%" == "Y" ( + SET RUNSETUP=Y +) IF "%RUNSETUP%"=="Y" ( %SETUP% ^ diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index e179239514..f3e4cec0b9 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1058,13 +1058,18 @@ function copq_coq_gtk { install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes" # This below item look like a bug in make install + if [ -d "$PREFIXCOQ/share/coq/" ] ; then + COQSHARE="$PREFIXCOQ/share/coq/" + else + COQSHARE="$PREFIXCOQ/share/" + fi if [[ ! $COQ_VERSION == 8.4* ]] ; then - mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" - mv "$PREFIXCOQ/share/coq/"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" + mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" + mv "$COQSHARE"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" fi mkdir -p "$PREFIXCOQ/ide" - mv "$PREFIXCOQ/share/coq/"*.png "$PREFIXCOQ/ide" - rmdir "$PREFIXCOQ/share/coq" + mv "$COQSHARE"*.png "$PREFIXCOQ/ide" + rmdir "$PREFIXCOQ/share/coq" || true fi } @@ -1119,11 +1124,11 @@ function make_coq { then if [ "$INSTALLMODE" == "relocatable" ]; then # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path - logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man + ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man elif [ "$INSTALLMODE" == "absolute" ]; then - logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" else - logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" + ./configure -with-doc no -prefix "$PREFIXCOQ" fi # The windows resource compiler binary name is hard coded @@ -1134,17 +1139,17 @@ function make_coq { if [[ $COQ_VERSION == 8.4* ]] ; then log1 make else - log1 make $MAKE_OPT + make $MAKE_OPT fi if [ "$INSTALLMODE" == "relocatable" ]; then - logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" fi - log2 make install - log1 copy_coq_dlls + make install + copy_coq_dlls if [ "$INSTALLOCAML" == "Y" ]; then - log1 copy_coq_objects + copy_coq_objects fi copq_coq_gtk @@ -1267,7 +1272,7 @@ function get_cygwin_mingw_sources { function make_coq_installer { make_coq make_mingw_make - # get_cygwin_mingw_sources + get_cygwin_mingw_sources # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: # ocaml: ocaml + menhir + camlp5 + findlib diff --git a/dev/ci/README.md b/dev/ci/README.md new file mode 100644 index 0000000000..f4423558cc --- /dev/null +++ b/dev/ci/README.md @@ -0,0 +1,130 @@ +Continuous Integration for the Coq Proof Assistant +================================================== + +Changes to Coq are systematically tested for regression and compatibility +breakage on our Continuous Integration (CI) platforms *before* integration, +so as to ensure better robustness and catch problems as early as possible. +These tests include the compilation of several external libraries / plugins. + +This document contains information for both external library / plugin authors, +who might be interested in having their development tested, and for Coq +developers / contributors, who must ensure that they don't break these +external developments accidentally. + +*Remark:* the CI policy outlined in this document is susceptible to evolve and +specific accommodations are of course possible. + +Information for external library / plugin authors +------------------------------------------------- + +You are encouraged to consider submitting your development for addition to +our CI. This means that: + +- Any time that a proposed change is breaking your development, Coq developers + will send you patches to adapt it or, at the very least, will work with you + to see how to adapt it. + +On the condition that: + +- At the time of the submission, your development works with Coq master branch. + +- Your development is publicly available in a git repository and we can easily + send patches to you (e.g. through pull / merge requests). + +- You react in a timely manner to discuss / integrate those patches. + +- You do not push, to the branches that we test, commits that haven't been + first tested to compile with the corresponding branch(es) of Coq. + +- Your development compiles in less than 35 minutes with just two threads. + If this is not the case, consider adding a "lite" target that compiles just + part of it. + +In case you forget to comply with these last three conditions, we would reach +out to you and give you a 30-day grace period during which your development +would be moved into our "allow failure" category. At the end of the grace +period, in the absence of progress, the development would be removed from our +CI. + +### Add your development by submitting a pull request + +Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at +[`ci-coq-dpdgraph.sh`](/dev/ci/ci-coq-dpdgraph.sh) or +[`ci-fiat-parsers.sh`](/dev/ci/ci-fiat-parsers.sh) for simple examples); +set the corresponding variables in +[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding +target to [`Makefile.ci`](/Makefile.ci); add new jobs to +[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that +this new target is run. **Do not hesitate to submit an incomplete pull request +if you need help to finish it.** + +You may also be interested in having your development tested in our +performance benchmark. Currently this is done by providing an OPAM package +in https://github.com/coq/opam-coq-archive and opening an issue at +https://github.com/coq/coq-bench/issues. + + +Information for developers +-------------------------- + +When you submit a pull request (PR) on Coq GitHub repository, this will +automatically launch a battery of CI tests. The PR will not be integrated +unless these tests pass. + +Currently, we have two CI platforms: + +- Travis is the main CI platform. It tests the compilation of Coq, of the + documentation, and of CoqIDE on Linux with several versions of OCaml / + camlp5, and with warnings as errors; it runs the test-suite and tests the + compilation of several external developments. It also tests the compilation + of Coq on OS X. + +- AppVeyor is used to test the compilation of Coq and run the test-suite on + Windows. + +You can anticipate the results of these tests prior to submitting your PR +by having them run of your fork of Coq, on GitHub or GitLab. This can be +especially helpful given that our Travis platform is often overloaded and +therefore there can be a significant delay before these tests are actually +run on your PR. To take advantage of this, simply create a Travis account +and link it to your GitHub account, or activate the pipelines on your GitLab +fork. + +You can also run one CI target locally (using `make ci-somedev`). + +Whenever your PR breaks tested developments, you should either adapt it +so that it doesn't, or provide a branch fixing these developments (or at +least work with the author of the development / other Coq developers to +prepare these fixes). Then, add an overlay in +[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) +in a separate commit in your PR. + +The process to merge your PR is then to submit PRs to the external +development repositories, merge the latter first (if the fixes are +backward-compatible), drop the overlay commit and merge the PR on Coq then. + + +Travis specific information +--------------------------- + +Travis rebuilds all of Coq's executables and stdlib for each job. Coq +is built with `./configure -local`, then used for the job's test. + + +GitLab specific information +--------------------------- + +GitLab is set up to use the "build artifact" feature to avoid +rebuilding Coq. In one job, Coq is built with `./configure -prefix +install` and `make install` is run, then the `install` directory +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 + architecture and Ocaml version used to build Coq. +- the Coq documentation, in two different copies varying in the OCaml + version used to build Coq + +As an exception to the above, jobs testing that compilation triggers +no Ocaml warnings build Coq in parallel with other tests. diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat new file mode 100644 index 0000000000..ca6a5643c1 --- /dev/null +++ b/dev/ci/appveyor.bat @@ -0,0 +1,35 @@ +REM This script either runs the test suite with OPAM (if USEOPAM is true) or +REM builds the Coq binary packages for windows (if USEOPAM is false). + +if %ARCH% == 32 ( + SET ARCHLONG=i686 + SET CYGROOT=C:\cygwin + SET SETUP=setup-x86.exe +) + +if %ARCH% == 64 ( + SET ARCHLONG=x86_64 + SET CYGROOT=C:\cygwin64 + SET SETUP=setup-x86_64.exe +) + +SET CYGCACHE=%CYGROOT%\var\cache\setup +SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/% +SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/% +SET DESTCOQ=C:\coq%ARCH%_inst +SET COQREGTESTING=Y + +if %USEOPAM% == false ( + call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ + -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ + -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -setup %CYGROOT%\%SETUP% + copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis + 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* +) + +if %USEOPAM% == true ( + %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^ + -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time + %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh +) diff --git a/dev/build/windows/appveyor.sh b/dev/ci/appveyor.sh index 53f7a23466..524a55a423 100644 --- a/dev/build/windows/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,8 +1,9 @@ #!/bin/bash set -e -x -wget $opam_url +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c eval $(opam config env) opam install -y ocamlfind camlp5 +cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 6560305433..8e7265969b 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -85,8 +85,8 @@ ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=trunk__API} -: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git} +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} ######################################################################## # fiat_crypto @@ -114,7 +114,9 @@ ######################################################################## # SF ######################################################################## -: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz} +: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz} +: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz} +: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz} ######################################################################## # TLC @@ -125,5 +127,5 @@ ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=master} -: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} +: ${bignums_CI_BRANCH:=fix-thunk-printer} +: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git} diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 238960948d..358f527f9e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -4,7 +4,7 @@ set -xe if [ -n "${GITLAB_CI}" ]; then - export COQBIN=`pwd`/install/bin + export COQBIN=`pwd`/_install_ci/bin else export COQBIN=`pwd`/bin fi diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index e8018158bf..b610f70004 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c9..1bf6e9a872 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 6e6c7012b7..272041205c 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -4,11 +4,18 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh # XXX: Needs fixing to properly set the build directory. -wget ${sf_CI_TARURL} -tar xvfz sf.tgz +wget ${sf_lf_CI_TARURL} +wget ${sf_plf_CI_TARURL} +wget ${sf_vfa_CI_TARURL} +tar xvfz lf.tgz +tar xvfz plf.tgz +tar xvfz vfa.tgz -sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v +sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v +sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v -( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) +( cd lf && make clean && make ) +( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) +( cd vfa && make clean && make ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh new file mode 100755 index 0000000000..96acc5a11c --- /dev/null +++ b/dev/ci/ci-wrapper.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +# Use this script to preserve the exit code of $CI_SCRIPT when piping +# it to `tee time-of-build.log`. We have a separate script, because +# this only works in bash, which we don't require project-wide. + +set -eo pipefail + +function travis_fold { + if [ -n "${TRAVIS}" ]; + then + echo "travis_fold:$1:$2" + fi +} + +CI_SCRIPT="$1" +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +# assume this script is in dev/ci/, cd to the root Coq directory +cd "${DIR}/../.." + +"${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log +travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +python ./tools/make-one-time-file.py time-of-build.log +travis_fold 'end' 'coq.test.timing' diff --git a/dev/core.dbg b/dev/core.dbg index 71d06cdb0a..18e82c352c 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,7 +16,6 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer highparsing.cma load_printer intf.cma load_printer API.cma load_printer ltac_plugin.cmo diff --git a/dev/db_printers.ml b/dev/db_printers.ml deleted file mode 100644 index f4b4a425e2..0000000000 --- a/dev/db_printers.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -open Pp -open Names - -let pp s = pp (hov 0 s) - -let prid id = Format.print_string (Id.to_string id) -let prsp sp = Format.print_string (DirPath.to_string sp) - - diff --git a/dev/doc/api.txt b/dev/doc/api.txt deleted file mode 100644 index 5827257b53..0000000000 --- a/dev/doc/api.txt +++ /dev/null @@ -1,10 +0,0 @@ -Recommendations in using the API: - -The type of terms: constr (see kernel/constr.ml and kernel/term.ml) - -- On type constr, the canonical equality on CIC (up to - alpha-conversion and cast removal) is Constr.equal -- The type constr is abstract, use mkRel, mkSort, etc. to build - elements in constr; use "kind_of_term" to analyze the head of a - constr; use destRel, destSort, etc. when the head constructor is - known diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index fefcb0937a..f3fc13e969 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -74,25 +74,25 @@ The Makefile is separated in several files : - Makefile.doc : specific rules for compiling the documentation. -FIND_VCS_CLAUSE +FIND_SKIP_DIRS --------------- -The recommended style of using FIND_VCS_CLAUSE is for example +The recommended style of using FIND_SKIP_DIRS is for example - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print 1) The parentheses even in the one-criteria case is so that if one adds other conditions, e.g. change the first example to the second - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print one is not tempted to write - find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print + find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print -because this will not necessarily work as expected; $(FIND_VCS_CLAUSE) +because this will not necessarily work as expected; $(FIND_SKIP_DIRS) ends with an -or, and how it combines with what comes later depends on operator precedence and all that. Much safer to override it with parentheses. @@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why. You are used to write: find . -name '*.example' and it works fine. But the following will not: - find . $(FIND_VCS_CLAUSE) -name '*.example' -it will also list things directly matched by FIND_VCS_CLAUSE + find . $(FIND_SKIP_DIRS) -name '*.example' +it will also list things directly matched by FIND_SKIP_DIRS (directories we want to prune, in which we don't want to find anything). C'est subtil... Il y a effectivement un -print implicite à la fin, qui fait que la commande habituelle sans print fonctionne bien, mais dès que l'on introduit d'autres commandes dans le lot (le --prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de +-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de parenthèses du -print implicite par rapport au parenthésage dans la forme recommandée d'utilisation: diff --git a/dev/doc/changes.txt b/dev/doc/changes.md index 57c7a97d58..5ed74917aa 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.md @@ -1,137 +1,146 @@ -========================================= -= CHANGES BETWEEN COQ V8.7 AND COQ V8.8 = -========================================= +## Changes between Coq 8.7 and Coq 8.8 -* ML API * +### Plugin API + +Coq 8.8 offers a new module overlay containing a proposed plugin API +in `API/API.ml`; this overlay is enabled by adding the `-open API` +flag to the OCaml compiler; this happens automatically for +developments in the `plugin` folder and `coq_makefile`. + +However, `coq_makefile` can be instructed not to enable this flag by +passing `-bypass-API`. + +### ML API We removed the following functions: -- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context +- `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` instead. The returned term contains De Bruijn universe variables. If you don't depend on universes being instantiated, simply drop the context. -- Universes.unsafe_type_of_global: same as above with - Global.type_of_global_in_context + +- `Universes.unsafe_type_of_global`: same as above with + `Global.type_of_global_in_context` We changed the type of the following functions: -- Global.body_of_constant_body: now also returns the abstract universe context. +- `Global.body_of_constant_body`: now also returns the abstract universe context. The returned term contains De Bruijn universe variables. -- Global.body_of_constant: same as above. -========================================= -= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = -========================================= +- `Global.body_of_constant`: same as above. -* Ocaml * +We renamed the following datatypes: -Coq is compiled with -safe-string enabled and requires plugins to do -the same. This means that code using `String` in an imperative way -will fail to compile now. They should switch to `Bytes.t` +- `Pp.std_ppcmds` -> `Pp.t` -* Plugin API * +## Changes between Coq 8.6 and Coq 8.7 -Coq 8.7 offers a new module overlay containing a proposed plugin API -in `API/API.ml`; this overlay is enabled by adding the `-open API` -flag to the OCaml compiler; this happens automatically for -developments in the `plugin` folder and `coq_makefile`. +### Ocaml -However, `coq_makefile` can be instructed not to enable this flag by -passing `-bypass-API`. +Coq is compiled with `-safe-string` enabled and requires plugins to do +the same. This means that code using `String` in an imperative way +will fail to compile now. They should switch to `Bytes.t` -* ML API * +### ML API -Added two functions for declaring hooks to be executed in reduction +- Added two functions for declaring hooks to be executed in reduction functions when some given constants are traversed: - declare_reduction_effect: to declare a hook to be applied when some + * `declare_reduction_effect`: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv). - set_reduction_effect: to declare a constant on which a given effect + * `set_reduction_effect`: to declare a constant on which a given effect hook should be called. -We renamed the following functions: +- We renamed the following functions: + ``` Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr Printer.pr_var_list_decl -> Printer.pr_compacted_decl Printer.pr_var_decl -> Printer.pr_named_decl Nameops.lift_subscript -> Nameops.increment_subscript + ``` -We removed the following functions: +- We removed the following functions: - Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context - Namegen.to_avoid ... equivalent substitute is Names.Id.List.mem + * `Termops.compact_named_context_reverse`: practical substitute is `Termops.compact_named_context`. + * `Namegen.to_avoid`: equivalent substitute is `Names.Id.List.mem`. -We renamed the following modules: +- We renamed the following modules: - Context.ListNamed -> Context.Compacted + * `Context.ListNamed` -> `Context.Compacted` -The following type aliases where removed +- The following type aliases where removed - Context.section_context ... it was just an alias for "Context.Named.t" which is still available + * `Context.section_context`: it was just an alias for `Context.Named.t` which is still available. -The module Constrarg was merged into Stdarg. +- The module `Constrarg` was merged into `Stdarg`. -The following types have been moved and modified: +- The following types have been moved and modified: - local_binder -> local_binder_expr - glob_binder merged with glob_decl + * `local_binder` -> `local_binder_expr` + * `glob_binder` merged with `glob_decl` -The following constructors have been renamed: +- The following constructors have been renamed: + ``` LocalRawDef -> CLocalDef LocalRawAssum -> CLocalAssum LocalPattern -> CLocalPattern + ``` -In Constrexpr_ops: +- In `Constrexpr_ops`: - Deprecating abstract_constr_expr in favor of mkCLambdaN, and - prod_constr_expr in favor of mkCProdN. Note: the first ones were - interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second + Deprecating `abstract_constr_expr` in favor of `mkCLambdaN`, and + `prod_constr_expr` in favor of `mkCProdN`. Note: the first ones were + interpreting `(x y z:_)` as `(x:_) (y:_) (z:_)` while the second ones were preserving the original sharing of the type. -In Nameops: +- In `Nameops`: The API has been made more uniform. New combinators added in the - "Name" space name. Function "out_name" now fails with IsAnonymous - rather than with Failure "Nameops.out_name". + `Name` space name. Function `out_name` now fails with `IsAnonymous` + rather than with `Failure "Nameops.out_name"`. -Location handling and AST attributes: +- Location handling and AST attributes: - Location handling has been reworked. First, Loc.ghost has been + Location handling has been reworked. First, `Loc.ghost` has been removed in favor of an option type, all objects carrying an optional source code location have been switched to use `Loc.t option`. Storage of location information has been also refactored. The main - datatypes representing Coq AST (constrexpr, glob_expr) have been + datatypes representing Coq AST (`constrexpr`, `glob_expr`) have been switched to a generic "node with attributes" representation `'a CAst.ast`, which is a record of the form: -```ocaml -type 'a ast = private { - v : 'a; - loc : Loc.t option; - ... -} -``` + ```ocaml + type 'a ast = private { + v : 'a; + loc : Loc.t option; + ... + } + ``` consumers of AST nodes are recommended to use accessor-based pattern matching `{ v; loc }` to destruct `ast` object. Creation is done with `CAst.make ?loc obj`, where the attributes are optional. Some convenient combinators are provided in the module. A typical match: -``` -| CCase(loc, a1) -> CCase(loc, f a1) -``` + + ```ocaml + | CCase(loc, a1) -> CCase(loc, f a1) + ``` + is now done as: -``` -| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) -``` + ```ocaml + | { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) + + ``` or even better, if plan to preserve the attributes you can wrap your top-level function in `CAst.map` to have: -``` -| CCase(a1) -> CCase(f a1) -``` + ```ocaml + | CCase(a1) -> CCase(f a1) + ``` This scheme based on records enables easy extensibility of the AST node type without breaking compatibility. @@ -147,14 +156,14 @@ type 'a ast = private { implemented in the whole code base. Matching a located object hasn't changed, however, `Loc.tag ?loc obj` must be used to build one. -In GOption: +- In `GOption`: Support for non-synchronous options has been removed. Now all options are handled as a piece of normal document state, and thus passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. -In Coqlib / reference location: +- In `Coqlib` / reference location: We have removed from Coqlib functions returning `constr` from names. Now it is only possible to obtain references, that must be @@ -171,62 +180,67 @@ In Coqlib / reference location: `pf_constr_of_global` in tactics and `Evarutil.new_global` variants when constructing terms in ML (see univpoly.txt for more information). -** Tactic API ** +### Tactic API -- pf_constr_of_global now returns a tactic instead of taking a continuation. +- `pf_constr_of_global` now returns a tactic instead of taking a continuation. Thus it only generates one instance of the global reference, and it is the caller's responsibility to perform a focus on the goal. -- pf_global, construct_reference, global_reference, - global_reference_in_absolute_module now return a global_reference - instead of a constr. +- `pf_global`, `construct_reference`, `global_reference`, + `global_reference_in_absolute_module` now return a `global_reference` + instead of a `constr`. -- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase - was very specific. Use tclPROGRESS instead. +- The `tclWEAK_PROGRESS` and `tclNOTSAMEGOAL` tacticals were removed. Their usecase + was very specific. Use `tclPROGRESS` instead. -- The unsafe flag of the Refine.refine function and its variants has been +- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows + to iterate a non-unit tactic on all goals and access their returned values. + +- The unsafe flag of the `Refine.refine` function and its variants has been renamed and dualized into typecheck and has been made mandatory. -** Ltac API ** +### Ltac API Many Ltac specific API has been moved in its own ltac/ folder. Amongst other important things: -- Pcoq.Tactic -> Pltac -- Constrarg.wit_tactic -> Tacarg.wit_tactic -- Constrarg.wit_ltac -> Tacarg.wit_ltac -- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument +- `Pcoq.Tactic` -> `Pltac` +- `Constrarg.wit_tactic` -> `Tacarg.wit_tactic` +- `Constrarg.wit_ltac` -> `Tacarg.wit_ltac` +- API below `ltac/` that accepted a *`_tactic_expr` now accept a *`_generic_argument` instead -- Some printing functions were moved from Pptactic to Pputils -- A part of Tacexpr has been moved to Tactypes -- The TacFun tactic expression constructor now takes a `Name.t list` for the +- Some printing functions were moved from `Pptactic` to `Pputils` +- A part of `Tacexpr` has been moved to `Tactypes` +- The `TacFun` tactic expression constructor now takes a `Name.t list` for the variable list rather than an `Id.t option list`. The folder itself has been turned into a plugin. This does not change much, but because it is a packed plugin, it may wreak havoc for third-party plugins -depending on any module defined in the ltac/ directory. Namely, even if +depending on any module defined in the `ltac/` directory. Namely, even if everything looks OK at compile time, a plugin can fail to load at link time -because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +because it mistakenly looks for a module `Foo` instead of `Ltac_plugin.Foo`, with an error of the form: +``` Error: while loading myplugin.cmxs, no implementation available for Foo. +``` -In particular, most EXTEND macros will trigger this problem even if they +In particular, most `EXTEND` macros will trigger this problem even if they seemingly do not use any Ltac module, as their expansion do. -The solution is simple, and consists in adding a statement "open Ltac_plugin" +The solution is simple, and consists in adding a statement `open Ltac_plugin` in each file using a Ltac module, before such a module is actually called. An alternative solution would be to fully qualify Ltac modules, e.g. turning any -call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not -work for EXTEND macros though. +call to Tacinterp into `Ltac_plugin.Tacinterp`. Note that this solution does not +work for `EXTEND` macros though. -** Additional changes in tactic extensions ** +### Additional changes in tactic extensions -Entry "constr_with_bindings" has been renamed into -"open_constr_with_bindings". New entry "constr_with_bindings" now +Entry `constr_with_bindings` has been renamed into +`open_constr_with_bindings`. New entry `constr_with_bindings` now uses type classes and rejects terms with unresolved holes. -** Error handling ** +### Error handling - All error functions now take an optional parameter `?loc:Loc.t`. For functions that used to carry a suffix `_loc`, such suffix has been @@ -236,14 +250,14 @@ uses type classes and rejects terms with unresolved holes. - The header parameter to `user_err` has been made optional. -** Pretty printing ** +### Pretty printing Some functions have been removed, see pretty printing below for more details. -* Pretty Printing and XML protocol * +#### Pretty Printing and XML protocol -The type std_cmdpps has been reworked and made the canonical "Coq rich +The type `std_cmdpps` has been reworked and made the canonical "Coq rich document type". This allows for a more uniform handling of printing (specially in IDEs). The main consequences are: @@ -260,12 +274,13 @@ document type". This allows for a more uniform handling of printing - `Pp_control` has removed. The new module `Topfmt` implements console control for the toplevel. - - The impure tag system in Pp has been removed. This also does away + - The impure tag system in `Pp` has been removed. This also does away with the printer signatures and functors. Now printers tag unconditionally. - The following functions have been removed from `Pp`: + ```ocaml val stras : int * string -> std_ppcmds val tbrk : int * int -> std_ppcmds val tab : unit -> std_ppcmds @@ -287,8 +302,9 @@ document type". This allows for a more uniform handling of printing val msg_with : ... module Tag + ``` -** Stm API ** +### Stm API - We have streamlined the `Stm` API, now `add` and `query` take a `coq_parsable` instead a `string` so clients can have more control @@ -305,7 +321,7 @@ document type". This allows for a more uniform handling of printing - A few unused hooks were removed due to cleanups, no clients known. -** Toplevel and Vernacular API ** +### Toplevel and Vernacular API - The components related to vernacular interpretation have been moved to their own folder `vernac/` whereas toplevel now contains the @@ -314,39 +330,41 @@ document type". This allows for a more uniform handling of printing - Coq's toplevel has been ported to directly use the common `Stm` API. The signature of a few functions has changed as a result. -** XML Protocol ** +### XML Protocol - The legacy `Interp` call has been turned into a noop. - The `query` call has been modified, now it carries a mandatory - "route_id" integer parameter, that associated the result of such + `route_id` integer parameter, that associated the result of such query with its generated feedback. -========================================= -= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = -========================================= +## Changes between Coq 8.5 and Coq 8.6 -** Parsing ** +### Parsing -Pcoq.parsable now takes an extra optional filename argument so as to +`Pcoq.parsable` now takes an extra optional filename argument so as to bind locations to a file name when relevant. -** Files ** +### Files To avoid clashes with OCaml's compiler libs, the following files were renamed: + +``` kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} lib/errors.ml{,i} -> lib/cErrors.ml{,i} toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} +``` -All IDE-specific files, including the XML protocol have been moved to ide/ +All IDE-specific files, including the XML protocol have been moved to `ide/` -** Reduction functions ** +### Reduction functions -In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, -fCOFIX. +In `closure.ml`, we introduced the more precise reduction flags `fMATCH`, `fFIX`, +`fCOFIX`. We renamed the following functions: +``` Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta @@ -373,9 +391,11 @@ Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all +``` And removed the following ones: +``` Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state @@ -385,15 +405,16 @@ Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta +``` -In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and -FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. +In `intf/genredexpr.mli`, `fIota` was replaced by `FMatch`, `FFix` and +`FCofix`. Similarly, `rIota` was replaced by `rMatch`, `rFix` and `rCofix`. -** Notation_ops ** +### Notation_ops -Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. +Use `Glob_ops.glob_constr_eq` instead of `Notation_ops.eq_glob_constr`. -** Logging and Pretty Printing: ** +### Logging and Pretty Printing * Printing functions have been removed from `Pp.mli`, which is now a purely pretty-printing interface. Functions affected are: @@ -422,7 +443,7 @@ val message : string -> unit * Feedback related functions and definitions have been moved to the `Feedback` module. `message_level` has been renamed to - level. Functions moved from Pp to Feedback are: + level. Functions moved from `Pp` to `Feedback` are: ```` ocaml val set_logger : logger -> unit @@ -467,12 +488,13 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit val get_id_for_feedback : unit -> edit_or_state_id * route_id ```` -** Kernel API changes ** +### Kernel API changes -- The interface of the Context module was changed. +- The interface of the `Context` module was changed. Related types and functions were put in separate submodules. The mapping from old identifiers to new identifiers is the following: + ``` Context.named_declaration ---> Context.Named.Declaration.t Context.named_list_declaration ---> Context.NamedList.Declaration.t Context.rel_declaration ---> Context.Rel.Declaration.t @@ -514,123 +536,142 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Context.rel_context_length ---> Context.Rel.length Context.rel_context_nhyps ---> Context.Rel.nhyps Context.rel_context_tags ---> Context.Rel.to_tags + ``` - Originally, rel-context was represented as: - Context.rel_context = Names.Name.t * Constr.t option * Constr.t + ```ocaml + type Context.rel_context = Names.Name.t * Constr.t option * Constr.t + ``` Now it is represented as: - Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t - + ```ocaml + type Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t + | LocalDef of Names.Name.t * Constr.t * Constr.t + ``` + - Originally, named-context was represented as: - Context.named_context = Names.Id.t * Constr.t option * Constr.t + ```ocaml + type Context.named_context = Names.Id.t * Constr.t option * Constr.t + ``` Now it is represented as: - Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t + ```ocaml + type Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t + | LocalDef of Names.Id.t * Constr.t * Constr.t + ``` -- The various EXTEND macros do not handle specially the Coq-defined entries +- The various `EXTEND` macros do not handle specially the Coq-defined entries anymore. Instead, they just output a name that have to exist in the scope - of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for - variables "$name" of type Gram.entry, while the parsing rules of - (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will - look for variables "wit_$name" of type Genarg.genarg_type. The small DSL + of the ML code. The parsing rules (`VERNAC`) `ARGUMENT EXTEND` will look for + variables `$name` of type `Gram.entry`, while the parsing rules of + (`VERNAC COMMAND` | `TACTIC`) `EXTEND`, as well as the various `TYPED AS` clauses will + look for variables `wit_$name` of type `Genarg.genarg_type`. The small DSL for constructing compound entries still works over this scheme. Note that in - the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound + the case of (`VERNAC`) `ARGUMENT EXTEND`, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. - For example, to get "wit_constr" you must "open Constrarg" at the top of the file. + For example, to get `wit_constr` you must `open Constrarg` at the top of the file. -- Evarutil was split in two parts. The new Evardefine file exposes functions -define_evar_* mostly used internally in the unification engine. +- `Evarutil` was split in two parts. The new `Evardefine` file exposes functions + `define_evar_`* mostly used internally in the unification engine. -- The Refine module was move out of Proofview. +- The `Refine` module was moved out of `Proofview`. + ``` Proofview.Refine.* ---> Refine.* + ``` -- A statically monotonous evarmap type was introduced in Sigma. Not all the API +- A statically monotonic evarmap type was introduced in `Sigma`. Not all the API has been converted, so that the user may want to use compatibility functions - Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when + `Sigma.to_evar_map` and `Sigma.Unsafe.of_evar_map` or `Sigma.Unsafe.of_pair` when needed. Code can be straightforwardly adapted in the following way: + ```ocaml let (sigma, x1) = ... in ... let (sigma, xn) = ... in (sigma, ans) + ``` should be turned into: + ```ocaml open Sigma.Notations let Sigma (x1, sigma, p1) = ... in ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + ``` Examples of `Sigma.Unsafe.of_evar_map` include: + ``` Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty + ``` -- The Proofview.Goal.*enter family of functions now takes a polymorphic +- The `Proofview.Goal.`*`enter` family of functions now takes a polymorphic continuation given as a record as an argument. + ```ocaml Proofview.Goal.enter begin fun gl -> ... end + ``` should be turned into + ```ocaml open Proofview.Notations Proofview.Goal.enter { enter = begin fun gl -> ... end } + ``` - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` - `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` - `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` - (`Global.named_context` ---> `Global.named_context_val`) - (`Context.Named.lookup` ---> `Environ.lookup_named_val`) +- `Global.named_context` ---> `Global.named_context_val` +- `Context.Named.lookup` ---> `Environ.lookup_named_val` -** Search API ** +### Search API The main search functions now take a function iterating over the results. This allows for clients to use streaming or more economic printing. -========================================= -= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = -========================================= +## Changes between Coq 8.4 and Coq 8.5 -** Refactoring : more mli interfaces and simpler grammar.cma ** +### Refactoring : more mli interfaces and simpler grammar.cma - A new directory intf/ now contains mli-only interfaces : - Constrexpr : definition of constr_expr, was in Topconstr - Decl_kinds : now contains binding_kind = Explicit | Implicit - Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind - Extend : was parsing/extend.mli - Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag - Glob_term : definition of glob_constr - Locus : definition of occurrences and stuff about clauses - Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ... - Notation_term : contains notation_constr, was Topconstr.aconstr - Pattern : contains constr_pattern - Tacexpr : was tactics/tacexpr.ml - Vernacexpr : was toplevel/vernacexpr.ml + * `Constrexpr` : definition of `constr_expr`, was in `Topconstr` + * `Decl_kinds` : now contains `binding_kind = Explicit | Implicit` + * `Evar_kinds` : type `Evar_kinds.t` was previously `Evd.hole_kind` + * `Extend` : was `parsing/extend.mli` + * `Genredexpr` : regroup `Glob_term.red_expr_gen` and `Tacexpr.glob_red_flag` + * `Glob_term` : definition of `glob_constr` + * `Locus` : definition of occurrences and stuff about clauses + * `Misctypes` : `intro_pattern_expr`, `glob_sort`, `cast_type`, `or_var`, ... + * `Notation_term` : contains `notation_constr`, was `Topconstr.aconstr` + * `Pattern` : contains `constr_pattern` + * `Tacexpr` : was `tactics/tacexpr.ml` + * `Vernacexpr` : was `toplevel/vernacexpr.ml` - Many files have been divided : - vernacexpr: vernacexpr.mli + Locality - decl_kinds: decl_kinds.mli + Kindops - evd: evar_kinds.mli + evd - tacexpr: tacexpr.mli + tacops - glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops - topconstr: constrexpr.mli + constrexpr_ops - + notation_expr.mli + notation_ops + topconstr - pattern: pattern.mli + patternops - libnames: libnames (qualid, reference) + globnames (global_reference) - egrammar: egramml + egramcoq + * vernacexpr: vernacexpr.mli + Locality + * decl_kinds: decl_kinds.mli + Kindops + * evd: evar_kinds.mli + evd + * tacexpr: tacexpr.mli + tacops + * glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops + * topconstr: constrexpr.mli + constrexpr_ops + + notation_expr.mli + notation_ops + topconstr + * pattern: pattern.mli + patternops + * libnames: libnames (qualid, reference) + globnames (global_reference) + * egrammar: egramml + egramcoq - New utility files : miscops (cf. misctypes.mli) and redops (cf genredexpr.mli). @@ -679,11 +720,11 @@ printing. letin_pat_tac do not accept a type anymore - New file find_subterm.ml for gathering former functions - subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now - take and outputs also an evar_map), and - subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now - renamed into replace_term_occ_modulo and - replace_term_occ_decl_modulo). + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl` (which now + take and outputs also an `evar_map`), and + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl_modulo` (now + renamed into `replace_term_occ_modulo` and + `replace_term_occ_decl_modulo`). - API of Inductiveops made more uniform (see commit log or file itself). @@ -697,36 +738,34 @@ printing. - All functions taking an env and a sigma (or an evdref) now takes the env first. -========================================= -= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = -========================================= +## Changes between Coq 8.3 and Coq 8.4 -** Functions in unification.ml have now the evar_map coming just after the env +- Functions in unification.ml have now the evar_map coming just after the env -** Removal of Tacinterp.constr_of_id ** +- Removal of Tacinterp.constr_of_id Use instead either global_reference or construct_reference in constrintern.ml. -** Optimizing calls to Evd functions ** +- Optimizing calls to Evd functions Evars are split into defined evars and undefined evars; for efficiency, when an evar is known to be undefined, it is preferable to use specific functions about undefined evars since these ones are generally fewer than the defined ones. -** Type changes in TACTIC EXTEND rules ** +- Type changes in TACTIC EXTEND rules Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained via Tacinterp.eval_tactic. -** ARGUMENT EXTEND ** +- ARGUMENT EXTEND It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED in ARGUMENT EXTEND statements. -** Renaming of rawconstr to glob_constr ** +- Renaming of rawconstr to glob_constr The "rawconstr" type has been renamed to "glob_constr" for consistency. The "raw" in everything related to former rawconstr has @@ -736,62 +775,67 @@ scripts to migrate code using Coq's internals, see commits 13743, 2010) in Subversion repository. Contribs have been fixed too, and commit messages there might also be helpful for migrating. -========================================= -= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = -========================================= +## Changes between Coq 8.2 and Coq 8.3 -** Light cleaning in evarutil.ml ** +### Light cleaning in evaruil.ml whd_castappevar is now whd_head_evar obsolete whd_ise disappears -** Restructuration of the syntax of binders ** +### Restructuration of the syntax of binders +``` binders_let -> binders binders_let_fixannot -> binders_fixannot binder_let -> closed_binder (and now covers only bracketed binders) binder was already obsolete and has been removed +``` -** Semantical change of h_induction_destruct ** +### Semantical change of h_induction_destruct Warning, the order of the isrec and evar_flag was inconsistent and has been permuted. Tactic induction_destruct in tactics.ml is unchanged. -** Internal tactics renamed +### Internal tactics renamed There is no more difference between bindings and ebindings. The following tactics are therefore renamed +``` apply_with_ebindings_gen -> apply_with_bindings_gen left_with_ebindings -> left_with_bindings right_with_ebindings -> right_with_bindings split_with_ebindings -> split_with_bindings +``` and the following tactics are removed -apply_with_ebindings (use instead apply_with_bindings) -eapply_with_ebindings (use instead eapply_with_bindings) + - apply_with_ebindings (use instead apply_with_bindings) + - eapply_with_ebindings (use instead eapply_with_bindings) -** Obsolete functions in typing.ml +### Obsolete functions in typing.ml For mtype_of, msort_of, mcheck, now use type_of, sort_of, check -** Renaming functions renamed +### Renaming functions renamed +``` concrete_name -> compute_displayed_name_in concrete_let_name -> compute_displayed_let_name_in rename_rename_bound_var -> rename_bound_vars_as_displayed lookup_name_as_renamed -> lookup_name_as_displayed next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away +``` -** Cleaning in commmand.ml +### Cleaning in commmand.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml Functions renamed: +``` declare_one_assumption -> declare_assumption declare_assumption -> declare_assumptions Command.syntax_definition -> Metasyntax.add_syntactic_definition @@ -808,15 +852,17 @@ instantiate_type_indrec_scheme -> weaken_sort_scheme instantiate_indrec_scheme -> modify_sort_scheme make_case_dep, make_case_nodep -> build_case_analysis_scheme make_case_gen -> build_case_analysis_scheme_default +``` Types: decl_notation -> decl_notation option -** Cleaning in libnames/nametab interfaces +### Cleaning in libnames/nametab interfaces Functions: +``` dirpath_prefix -> pop_dirpath extract_dirpath_prefix pop_dirpath_n extend_dirpath -> add_dirpath_suffix @@ -830,17 +876,19 @@ absolute_reference -> global_of_path locate_syntactic_definition -> locate_syndef path_of_syntactic_definition -> path_of_syndef push_syntactic_definition -> push_syndef +``` Types: section_path -> full_path -** Cleaning in parsing extensions (commit 12108) +### Cleaning in parsing extensions (commit 12108) Many moves and renamings, one new file (Extrawit, that contains wit_tactic). -** Cleaning in tactical.mli +### Cleaning in tactical.mli +``` tclLAST_HYP -> onLastHyp tclLAST_DECL -> onLastDecl tclLAST_NHYPS -> onNLastHypsId @@ -850,24 +898,21 @@ onLastHyp -> onLastHypId onNLastHyps -> onNLastDecls onClauses -> onClause allClauses -> allHypsAndConcl +``` -+ removal of various unused combinators on type "clause" - -========================================= -= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = -========================================= +and removal of various unused combinators on type "clause" -A few differences in Coq ML interfaces between Coq V8.1 and V8.2 -================================================================ +## Changes between Coq 8.1 and Coq 8.2 -** Datatypes +### Datatypes List of occurrences moved from "int list" to "Termops.occurrences" (an alias to "bool * int list") ETIdent renamed to ETName -** Functions +### Functions +``` Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply Tactics: apply_with_bindings -> apply_with_bindings_wo_evars Eauto.simplest_apply -> Hiddentac.h_simplest_apply @@ -877,98 +922,93 @@ Tactics.true_cut renamed into Tactics.assert_tac Constrintern.interp_constrpattern -> intern_constr_pattern Hipattern.match_with_conjunction is a bit more restrictive Hipattern.match_with_disjunction is a bit more restrictive +``` -** Universe names (univ.mli) +### Universe names (univ.mli) + ```ocaml base_univ -> type0_univ (* alias of Set is the Type hierarchy *) prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) is_base_univ -> is_type1_univ is_empty_univ -> is_lower_univ + ``` -** Sort names (term.mli) +### Sort names (term.mli) + ``` mk_Set -> set_sort mk_Prop -> prop_sort type_0 -> type1_sort - -========================================= -= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.0 and V8.1 -================================================================ - -** Functions - -Util: option_app -> option_map -Term: substl_decl -> subst_named_decl -Lib: library_part -> remove_section_part -Printer: prterm -> pr_lconstr -Printer: prterm_env -> pr_lconstr_env -Ppconstr: pr_sort -> pr_rawsort -Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) -Pretyping: - - understand_gen_tcc and understand_gen_ltac merged into understand_ltac - - type_constraints can now say typed by a sort (use OfType to get the - previous behavior) -Library: import_library -> import_module - -** Constructors - -Declarations: mind_consnrealargs -> mind_consnrealdecls -NoRedun -> NoDup -Cast and RCast have an extra argument: you can recover the previous + ``` + +## Changes between Coq 8.0 and Coq 8.1 + +### Functions + +- Util: option_app -> option_map +- Term: substl_decl -> subst_named_decl +- Lib: library_part -> remove_section_part +- Printer: prterm -> pr_lconstr +- Printer: prterm_env -> pr_lconstr_env +- Ppconstr: pr_sort -> pr_rawsort +- Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) +- Pretyping: + - understand_gen_tcc and understand_gen_ltac merged into understand_ltac + - type_constraints can now say typed by a sort (use OfType to get the + previous behavior) +- Library: import_library -> import_module + +### Constructors + + * Declarations: mind_consnrealargs -> mind_consnrealdecls + * NoRedun -> NoDup + * Cast and RCast have an extra argument: you can recover the previous behavior by setting the extra argument to "CastConv DEFAULTcast" and "DEFAULTcast" respectively -Names: "kernel_name" is now "constant" when argument of Term.Const -Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert -Tacexpr: TacForward(true,_,_) branched to TacLetTac + * Names: "kernel_name" is now "constant" when argument of Term.Const + * Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert + * Tacexpr: TacForward(true,_,_) branched to TacLetTac -** Modules +### Modules -module Decl_kinds: new interface -module Bigint: new interface -module Tacred spawned module Redexpr -module Symbols -> Notation -module Coqast, Ast, Esyntax, Termast, and all other modules related to old - syntax are removed -module Instantiate: integrated to Evd -module Pretyping now a functor: use Pretyping.Default instead + * module Decl_kinds: new interface + * module Bigint: new interface + * module Tacred spawned module Redexpr + * module Symbols -> Notation + * module Coqast, Ast, Esyntax, Termast, and all other modules related to old + syntax are removed + * module Instantiate: integrated to Evd + * module Pretyping now a functor: use Pretyping.Default instead -** Internal names +### Internal names OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE -** Tactic extensions +### Tactic extensions -- printers have an extra parameter which is a constr printer at high precedence -- the tactic printers have an extra arg which is the expected precedence -- level is now a precedence in declare_extra_tactic_pprule -- "interp" functions now of types the actual arg type, not its encapsulation - as a generic_argument + * printers have an extra parameter which is a constr printer at high precedence + * the tactic printers have an extra arg which is the expected precedence + * level is now a precedence in declare_extra_tactic_pprule + * "interp" functions now of types the actual arg type, not its encapsulation + as a generic_argument -========================================= -= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 = -========================================= +## Changes between Coq 7.4 and Coq 8.0 See files in dev/syntax-v8 -============================================== -= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 = -============================================== +## Main changes between Coq 7.4 and Coq 8.0 -CHANGES DUE TO INTRODUCTION OF MODULES -====================================== +### Changes due to introduction of modules -1.Kernel --------- +#### Kernel The module level has no effect on constr except for the structure of section_path. The type of unique names for constructions (what section_path served) is now called a kernel name and is defined by +```ocaml type uniq_ident = int * string * dir_path (* int may be enough *) type module_path = | MPfile of dir_path (* reference to physical module, e.g. file *) @@ -995,7 +1035,8 @@ type kernel_name = module_path * dir_path * label Def u = ... end Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a - +``` + <M> and <N> are self-references, X is a bound reference and L is a reference to a physical module. @@ -1012,14 +1053,13 @@ world. module_expr) and kernel/declarations.ml (type module_body and module_type_body). -2. Library ----------- +#### Library -i) tables +1. tables [Summaries] - the only change is the special treatment of the global environmet. -ii) objects +2. objects [Libobject] declares persistent objects, given with methods: * cache_function specifying how to add the object in the current @@ -1040,25 +1080,25 @@ Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal version such as (MPself<Datatypes#1>,[],"Fst") (see above) -What happens at the end of an interactive module ? -================================================== +#### What happens at the end of an interactive module ? + (or when a file is stored and reloaded from disk) All summaries (except Global environment) are reverted to the state from before the beginning of the module, and: -a) the objects (again, since last Declaremods.start_module or +1. the objects (again, since last Declaremods.start_module or Library.start_library) are classified using the classify_function. To simplify consider only those who returned Substitute _ or Keep _. -b) If the module is not a functor, the subst_function for each object of +2. If the module is not a functor, the subst_function for each object of the first group is called with the substitution [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"]. Then the load_function is called for substituted objects and the "keep" object. (If the module is a library the substitution is done at reloading). -c) The objects which returned substitute are stored in the modtab +3. The objects which returned substitute are stored in the modtab together with the self ident of the module, and functor argument names if the module was a functor. @@ -1068,9 +1108,9 @@ c) The objects which returned substitute are stored in the modtab is evaluated -The difference between "substitute" and "keep" objects -======================================================== -i) The "keep" objects can _only_ reference other objects by section_paths +#### The difference between "substitute" and "keep" objects + +1. The "keep" objects can _only_ reference other objects by section_paths and qualids. They do not need the substitution function. They will work after end_module (or reloading a compiled library), @@ -1082,7 +1122,7 @@ These would typically be grammar rules, pretty printing rules etc. -ii) The "substitute" objects can _only_ reference objects by +2. The "substitute" objects can _only_ reference objects by kernel_names. They must have a valid subst_function. They will work after end_module _and_ after Module Z:=N or @@ -1091,17 +1131,18 @@ Module Z:=F(M). Other kinds of objects: -iii) "Dispose" - objects which do not survive end_module + +3. "Dispose" - objects which do not survive end_module As a consequence, objects which reference other objects sometimes by kernel_names and sometimes by section_path must be of this kind... -iv) "Anticipate" - objects which must be treated individually by +4. "Anticipate" - objects which must be treated individually by end_module (typically "REQUIRE" objects) -Writing subst_thing functions -============================= +#### Writing subst_thing functions + The subst_thing shoud not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. @@ -1116,15 +1157,13 @@ They are all (apart from constr, for now) written in the non-copying way. -Nametab -======= +#### Nametab Nametab has been made more uniform. For every kind of thing there is only one "push" function and one "locate" function. -Lib -=== +#### Lib library_segment is now a list of object_name * library_item, where object_name = section_path * kernel_name (see above) @@ -1132,20 +1171,19 @@ object_name = section_path * kernel_name (see above) New items have been added for open modules and module types -Declaremods -========== +#### Declaremods + Functions to declare interactive and noninteractive modules and module types. -Library -======= +#### Library + Uses Declaremods to actually communicate with Global and to register objects. -OTHER CHANGES -============= +### Other changes Internal representation of tactics bindings has changed (see type Rawterm.substitution). @@ -1162,258 +1200,48 @@ New parsing model for tactics and vernacular commands TACTIC EXTEND ... END to be used in ML files New organisation of THENS: -tclTHENS tac tacs : tacs is now an array -tclTHENSFIRSTn tac1 tacs tac2 : + +- tclTHENS tac tacs : tacs is now an array +- tclTHENSFIRSTn tac1 tacs tac2 : apply tac1 then, apply the array tacs on the first n subgoals and tac2 on the remaining subgoals (previously tclTHENST) -tclTHENSLASTn tac1 tac2 tacs : +- tclTHENSLASTn tac1 tac2 tacs : apply tac1 then, apply tac2 on the first subgoals and apply the array tacs on the last n subgoals -tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) -tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs -tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] -tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) -tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") -tclTHENSV same as tclTHENS but with an array -tclTHENSi : no longer available +- tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) +- tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs +- tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] +- tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) +- tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") +- tclTHENSV same as tclTHENS but with an array +- tclTHENSi : no longer available Proof_type: subproof field in type proof_tree glued with the ref field Tacmach: no more echo from functions of module Refiner Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. + Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd VERNAC COMMAND EXTEND macros + File syntax/PPTactic.v moved to parsing/pptactic.ml + Tactics about False and not now in tactics/contradiction.ml + Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) + File tacinterp.ml moved from proofs to directory tactics -========================================== -= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 = -========================================== +## Changes between Coq 7.1 and Coq 7.2 The core of Coq (kernel) has meen minimized with the following effects: -kernel/term.ml split into kernel/term.ml, pretyping/termops.ml -kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml -kernel/names.ml split into kernel/names.ml, library/nameops.ml -kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml +- kernel/term.ml split into kernel/term.ml, pretyping/termops.ml +- kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml +- kernel/names.ml split into kernel/names.ml, library/nameops.ml +- kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors, e.g. IsRel is now Rel, IsMutCase is now Case, etc. - - -======================================================= -= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 = -======================================================= - -Changements d'organisation / modules : --------------------------------------- - - Std, More_util -> lib/util.ml - - Names -> kernel/names.ml et kernel/sign.ml - (les parties noms et signatures ont été séparées) - - Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) - Mhb -> Bij - - Generic est intégré à Term (et un petit peu à Closure) - -Changements dans les types de données : ---------------------------------------- - dans Generic: free_rels : constr -> int Listset.t - devient : constr -> Intset.t - - type_judgement -> typed_type - environment -> context - context -> typed_type signature - - -ATTENTION: ----------- - - Il y a maintenant d'autres exceptions que UserError (TypeError, - RefinerError, etc.) - - Il ne faut donc plus se contenter (pour rattraper) de faire - - try . .. with UserError _ -> ... - - mais écrire à la place - - try ... with e when Logic.catchable_exception e -> ... - - -Changements dans les fonctions : --------------------------------- - - Vectops. - it_vect -> Array.fold_left - vect_it -> Array.fold_right - exists_vect -> Util.array_exists - for_all2eq_vect -> Util.array_for_all2 - tabulate_vect -> Array.init - hd_vect -> Util.array_hd - tl_vect -> Util.array_tl - last_vect -> Util.array_last - it_vect_from -> array_fold_left_from - vect_it_from -> array_fold_right_from - app_tl_vect -> array_app_tl - cons_vect -> array_cons - map_i_vect -> Array.mapi - map2_vect -> array_map2 - list_of_tl_vect -> array_list_of_tl - - Names - sign_it -> fold_var_context (se fait sur env maintenant) - it_sign -> fold_var_context_reverse (sur env maintenant) - - Generic - noccur_bet -> noccur_between - substn_many -> substnl - - Std - comp -> Util.compose - rev_append -> List.rev_append - - Termenv - mind_specif_of_mind -> Global.lookup_mind_specif - ou Environ.lookup_mind_specif si on a un env sous la main - mis_arity -> instantiate_arity - mis_lc -> instantiate_lc - - Ex-Environ - mind_of_path -> Global.lookup_mind - - Printer - gentermpr -> gen_pr_term - term0 -> prterm_env - pr_sign -> pr_var_context - pr_context_opt -> pr_context_of - pr_ne_env -> pr_ne_context_of - - Typing, Machops - type_of_type -> judge_of_type - fcn_proposition -> judge_of_prop_contents - safe_fmachine -> safe_infer - - Reduction, Clenv - whd_betadeltat -> whd_betaevar - whd_betadeltatiota -> whd_betaiotaevar - find_mrectype -> Inductive.find_mrectype - find_minductype -> Inductive.find_inductive - find_mcoinductype -> Inductive.find_coinductive - - Astterm - constr_of_com_casted -> interp_casted_constr - constr_of_com_sort -> interp_type - constr_of_com -> interp_constr - rawconstr_of_com -> interp_rawconstr - type_of_com -> type_judgement_of_rawconstr - judgement_of_com -> judgement_of_rawconstr - - Termast - bdize -> ast_of_constr - - Tacmach - pf_constr_of_com_sort -> pf_interp_type - pf_constr_of_com -> pf_interp_constr - pf_get_hyp -> pf_get_hyp_typ - pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant) - - Pattern - raw_sopattern_of_compattern -> Astterm.interp_constrpattern - somatch -> is_matching - dest_somatch -> matches - - Tacticals - matches -> gl_is_matching - dest_match -> gl_matches - suff -> utiliser sort_of_goal - lookup_eliminator -> utiliser sort_of_goal pour le dernier arg - - Divers - initial_sign -> var_context - - Sign - ids_of_sign -> ids_of_var_context (or Environ.ids_of_context) - empty_sign -> empty_var_context - - Pfedit - list_proofs -> get_all_proof_names - get_proof -> get_current_proof_name - abort_goal -> abort_proof - abort_goals -> abort_all_proofs - abort_cur_goal -> abort_current_proof - get_evmap_sign -> get_goal_context/get_current_goal_context - unset_undo -> reset_undo - - Proof_trees - mkGOAL -> mk_goal - - Declare - machine_constant -> declare_constant (+ modifs) - - ex-Trad, maintenant Pretyping - inh_cast_rel -> Coercion.inh_conv_coerce_to - inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail - ise_resolve1 -> understand, understand_type - ise_resolve -> understand_judgment, understand_type_judgment - - ex-Tradevar, maintenant Evarutil - mt_tycon -> empty_tycon - - Recordops - struc_info -> find_structure - -Changements dans les inductifs ------------------------------- -Nouveaux types "constructor" et "inductive" dans Term -La plupart des fonctions de typage des inductives prennent maintenant -un inductive au lieu d'un oonstr comme argument. Les seules fonctions -à traduire un constr en inductive sont les find_rectype and co. - -Changements dans les grammaires -------------------------------- - - . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex - - . attention : LIDENT -> IDENT (les identificateurs n'ont pas de - casse particulière dans Coq) - - . Le mot "command" est remplacé par "constr" dans les noms de - fichiers, noms de modules et non-terminaux relatifs au parsing des - termes; aussi les changements suivants "COMMAND"/"CONSTR" dans - g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml* - - . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n - passent en minuscule Identifier, Constr, ... - - . Plusieurs parsers ont changé de format (ex: sortarg) - -Changements dans le pretty-printing ------------------------------------ - - . Découplage de la traduction de constr -> rawconstr (dans detyping) - et de rawconstr -> ast (dans termast) - . Déplacement des options d'affichage de printer vers termast - . Déplacement des réaiguillage d'univers du pp de printer vers esyntax - - -Changements divers ------------------- - - . il n'y a plus de script coqtop => coqtop et coqtop.byte sont - directement le résultat du link du code - => debuggage et profiling directs - - . il n'y a plus d'installation locale dans bin/$ARCH - - . #use "include.ml" => #use "include" - go() => loop() - - . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup - de temps diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 00e7f5c53c..2dbd132da7 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -14,11 +14,6 @@ parsing tactics toplevel -highparsing : - - Files in parsing/ that cannot be linked too early. - Contains the grammar rules g_*.ml4 - Special components ------------------ diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.md index 79cde48849..7e9373b294 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.md @@ -1,7 +1,7 @@ Debugging from Coq toplevel using Caml trace mechanism ====================================================== - 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) + 1. Launch bytecode version of Coq (coqtop.byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' 3. Install load paths and pretty printers for terms, idents, ... using Ocaml command '#use "base_include";;' (use '#use "include";;' for @@ -25,8 +25,9 @@ Debugging from Coq toplevel using Caml trace mechanism Debugging from Caml debugger ============================ - Needs tuareg mode in Emacs - Coq must be configured with -debug and -local (./configure -debug -local) + Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\ + Coq must be configured with `-local` (`./configure -local`) and the + byte-code version of `coqtop` must have been generated with `make byte`. 1. M-x camldebug 2. give the binary name bin/coqtop.byte @@ -53,6 +54,9 @@ Debugging from Caml debugger of each of error* functions or anomaly* functions in lib/util.ml - If "source db" fails, do a "make printers" and try again (it should build top_printers.cmo and the core cma files). + - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on + startup when run from the debugger. If this happens, unset the variable, + re-start Emacs, and run the debugger again. Global gprof-based profiling ============================ @@ -65,14 +69,14 @@ Global gprof-based profiling Per function profiling ====================== - 1. To profile function foo in file bar.ml, add the following lines, just - after the definition of the function: + To profile function foo in file bar.ml, add the following lines, just + after the definition of the function: let fookey = Profile.declare_profile "foo";; let foo a b c = Profile.profile3 fookey foo a b c;; - where foo is assumed to have three arguments (adapt using - Profile.profile1, Profile. profile2, etc). + where foo is assumed to have three arguments (adapt using + Profile.profile1, Profile. profile2, etc). - This has the effect to cumulate the time passed in foo under a - line of name "foo" which is displayed at the time coqtop exits. + This has the effect to cumulate the time passed in foo under a + line of name "foo" which is displayed at the time coqtop exits. diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v index a81f170c63..a81f170c63 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion.v diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel deleted file mode 100644 index ffdb1bdca9..0000000000 --- a/dev/tools/Makefile.devel +++ /dev/null @@ -1,74 +0,0 @@ -# to be linked to makefile (lowercase - takes precedence over Makefile) -# in main directory -# make devel in main directory should do this for you. - -TOPDIR=. -BASEDIR= - -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API - -default: usage noargument - -usage:: - @echo Usage: make \<target\> - @echo Targets are: - -usage:: - @echo " setup-devel -- set the devel makefile" -setup-devel: - @ln -sfv dev/tools/Makefile.devel makefile - @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ - done) - - -usage:: - @echo " clean-devel -- clear all devel files" -clean-devel: - echo rm -f makefile .depend.devel - echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile) - - -usage:: - @echo " coqtop -- make until the bytecode executable, make the link" -coqtop: bin/coqtop.byte - ln -sf bin/coqtop.byte coqtop - - -usage:: - @echo " quick -- make bytecode executable and states" -quick: - $(MAKE) states BEST=byte - -include Makefile - -include $(TOPDIR)/dev/tools/Makefile.common - -# this file is better described in dev/tools/Makefile.dir -include .depend.devel - -#if dev/tools/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) -include $(TOPDIR)/dev/tools/Makefile.local -endif - - -usage:: - @echo " total -- runs coqtop with all theories required" -total: - ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th)))) - - -usage:: - @echo " run -- makes and runs bytecode coqtop using ledit and the history file" - @echo " if you want to pass arguments to coqtop, use make run ARG=<args>" -run: $(TOPDIR)/coqtop - ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS) - - -usage:: - @echo " vars -- echos commands to set COQTOP and COQBIN variables" -vars: - @(cd $(TOPDIR); \ - echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ ) diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir deleted file mode 100644 index 1a1bb90b44..0000000000 --- a/dev/tools/Makefile.dir +++ /dev/null @@ -1,131 +0,0 @@ -# make a link to this file if you are working hard in one directory of Coq -# ln -s ../dev/tools/Makefile.dir Makefile -# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead -# this Makefile provides many useful facilities to develop Coq -# it is not completely compatible with .ml4 files unfortunately - -ifndef TOPDIR -TOPDIR=.. -endif - -# this complicated thing should work for subsubdirs as well -BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||")) - -noargs: dir - -test-dir: - @echo TOPDIR=$(TOPDIR) - @echo BASEDIR=$(BASEDIR) - -include $(TOPDIR)/dev/tools/Makefile.common - -# make this directory -dir: - $(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR)) - -# make all cmo's in this directory. Useful in case the main Makefile is not -# up-to-date -all: - @( ( for i in *.ml; do \ - echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ - done; \ - for i in *.ml4; do \ - echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \ - done ) \ - | xargs $(MAKE) -C $(TOPDIR) ) - -# lists all files that should be compiled in this directory -list: - @(for i in *.mli; do \ - ls -l `basename $$i .mli`.cmi; \ - done) - @(for i in *.ml; do \ - ls -l `basename $$i .ml`.cmo; \ - done) - @(for i in *.ml4; do \ - ls -l `basename $$i .ml4`.cmo; \ - done) - - -clean:: - rm -f *.cmi *.cmo *.cmx *.o - - -# if grammar.cmo files cannot be compiled and main .depend cannot be -# rebuilt, this is quite useful -depend: - (cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel) - - -# displays the dependency graph of the current directory (vertically, -# unlike in doc/) -graph: - (ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) & - - -# the pretty entry draws a dependency graph marking red those nodes -# which do not have their .cmo files - -.INTERMEDIATE: depend.dot depend.2.dot -.PHONY: depend.ps - -depend.dot: - ocamldep *.ml *.mli | ocamldot > $@ - -depend.2.dot: depend.dot - (i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@ - (for ml in *.ml; do \ - base=`basename $$ml .ml`; \ - fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \ - rest=`echo $$base | cut -c2-`; \ - name=`echo $$fst $$rest | tr -d " "`; \ - cmo=$$base.cmo; \ - if [ ! -e $$cmo ]; then \ - echo \"$$name\" [color=red]\; >> $@;\ - fi;\ - done;\ - echo } >> $@) - -depend.ps: depend.2.dot - dot -Tps $< > $@ - -clean:: - rm -f depend.ps - -pretty: depend.ps - (gv -spartan $<; rm $<) & -# gv -spartan $< & - - - -# generating file.ml.mli by tricking make to pass -i to ocamlc - -%.ml.mli: FORCE - @(cmo=`basename $@ .ml.mli`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \ - echo Generated interface file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -%.annot: FORCE - @(cmo=`basename $@ .annot`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \ - echo Generated annotation file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -FORCE: - -clean:: - rm -f *.ml.mli - -# this is not perfect but mostly WORKS! It just calls the main makefile - -%.cmi: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -%.cmo: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -coqtop: - $(MAKE) -C $(TOPDIR) bin/coqtop.byte diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir deleted file mode 100644 index cb914bd129..0000000000 --- a/dev/tools/Makefile.subdir +++ /dev/null @@ -1,7 +0,0 @@ -# if you work in a sub/sub-rectory of Coq -# you should make a link to that makefile -# ln -s ../../dev/tools/Makefile.subdir Makefile -# in order to have all the facilities of dev/tools/Makefile.dir - -TOPDIR=../.. -include $(TOPDIR)/dev/tools/Makefile.dir diff --git a/dev/v8-syntax/.gitignore b/dev/v8-syntax/.gitignore new file mode 100644 index 0000000000..89e3509b00 --- /dev/null +++ b/dev/v8-syntax/.gitignore @@ -0,0 +1,6 @@ +# byproducts of check-grammar +def +df +use +use-k +use-t diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index fa2864cec9..6b7960c92f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} |