diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Coq_Bugzilla_autolink.user.js | 34 | ||||
| -rwxr-xr-x | dev/build/osx/make-macos-dmg.sh | 7 | ||||
| -rw-r--r-- | dev/build/windows/MakeCoq_MinGW.bat | 20 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/ci/appveyor.bat | 14 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 3 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 6 | ||||
| -rw-r--r-- | dev/core.dbg | 1 | ||||
| -rw-r--r-- | dev/doc/changes.md (renamed from dev/doc/changes.txt) | 875 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 5 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 5 |
11 files changed, 414 insertions, 560 deletions
diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js new file mode 100644 index 0000000000..371c5adc00 --- /dev/null +++ b/dev/Coq_Bugzilla_autolink.user.js @@ -0,0 +1,34 @@ +// ==UserScript== +// @name Coq Bugzilla autolink +// @namespace SkySkimmer +// @include https://github.com/coq/coq/* +// @description Makes BZ#XXXX into links to bugzilla for GitHub +// @version 1 +// @grant none +// ==/UserScript== + +var regex = /BZ#(\d+)/g; +var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>'; + +function doNode(node) +{ + node.innerHTML = node.innerHTML.replace(regex,substr); +} + +var comments = document.getElementsByClassName("comment-body"); + +for(var i=0; i<comments.length; i++) +{ + var pars = comments[i].getElementsByTagName("p"); + for(var j=0; j<pars.length; j++) + { + doNode(pars[j]); + } +} + +// usually 1 or 0 titles... +var titles = document.getElementsByClassName("js-issue-title"); +for(var i=0; i<titles.length; i++) +{ + doNode(titles[i]); +} diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index cbe2a5186f..cfcc09b327 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -9,15 +9,12 @@ DMGDIR=$PWD/_dmg VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app -# Create a .app file with CoqIDE -make -j $NJOBS -l2 $APP +# Create a .app file with CoqIDE, without signing it +make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP # Add Coq to the .app file make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop -# Sign the .app file -codesign -f -s - $APP - # Create the dmg bundle mkdir -p $DMGDIR ln -sf /Applications $DMGDIR/Applications diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index a420b5d8bb..f91b301b8c 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -328,12 +328,6 @@ ECHO ========== INSTALL CYGWIN ========== REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES. REM Otherwise chmod won't work and e.g. the ocaml build will fail. REM Cygwin setup does not touch the ACLs of existing folders. -REM => Create the setup log in a temporary location and move it later. - -REM Get Unique temporary file name -:logfileloop -SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log -if exist "%LOGFILE%" GOTO logfileloop REM Run Cygwin Setup @@ -348,6 +342,12 @@ IF "%COQREGTESTING%" == "Y" ( SET RUNSETUP=Y ) +SET "EXTRAPACKAGES= " + +IF NOT "%APPVEYOR%" == "True" ( + SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5" +) + IF "%RUNSETUP%"=="Y" ( %SETUP% ^ --proxy "%PROXY%" ^ @@ -356,10 +356,9 @@ IF "%RUNSETUP%"=="Y" ( --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^ --no-shortcuts ^ %CYGWIN_OPT% ^ - -P wget,curl,git,make,unzip ^ - -P gcc-core,gcc-g++ ^ + -P make,unzip ^ -P gdb,liblzma5 ^ - -P patch,automake1.14,automake1.15 ^ + -P patch,automake1.14 ^ -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^ -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^ -P libiconv-devel,libunistring-devel,libncurses-devel ^ @@ -369,12 +368,11 @@ IF "%RUNSETUP%"=="Y" ( -P gtk-update-icon-cache ^ -P libtool,automake ^ -P intltool ^ - > "%LOGFILE%" ^ + %EXTRAPACKAGES% ^ || GOTO ErrorExit MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" - MOVE "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit ) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f3e4cec0b9..f12cbe0a78 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -910,6 +910,10 @@ function make_camlp5 { log2 make install # For some reason gramlib.a is not copied, but it is required by Coq cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" + # For some reason META is not copied, but it is required by coq_makefile + log2 make -C etc META + mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" + cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" log2 make clean build_post fi diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index ca6a5643c1..e2fbf1f6d1 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,13 +23,19 @@ 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\* + -setup %CYGROOT%\%SETUP% || GOTO ErrorExit + copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit + 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) 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 + %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit ) + +GOTO :EOF + +:ErrorExit + ECHO ERROR MakeCoq_MinGW.bat failed + EXIT /b 1 diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 238960948d..1bfdf7dfbe 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -4,7 +4,8 @@ set -xe if [ -n "${GITLAB_CI}" ]; then - export COQBIN=`pwd`/install/bin + export COQBIN=`pwd`/_install_ci/bin + export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" else export COQBIN=`pwd`/bin fi diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index eadeb7c38c..8e6448e764 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -8,9 +8,5 @@ GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} ( cd ${GeoCoq_CI_DIR} && \ - ./configure.sh && \ - sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ - sed -i.bak '/Elements\/Book_1\.v/d' Make && \ - sed -i.bak '/Elements\/Book_3\.v/d' Make && \ - coq_makefile -f Make -o Makefile && \ + ./configure-ci.sh && \ make ) 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/doc/changes.txt b/dev/doc/changes.md index 0f1a28028c..5ed74917aa 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.md @@ -1,141 +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. + +- `Global.body_of_constant`: same as above. We renamed the following datatypes: - Pp.std_ppcmds -> Pp.t +- `Pp.std_ppcmds` -> `Pp.t` -========================================= -= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = -========================================= +## Changes between Coq 8.6 and Coq 8.7 -* Ocaml * +### Ocaml -Coq is compiled with -safe-string enabled and requires plugins to do +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` -* Plugin API * +### ML API -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`. - -However, `coq_makefile` can be instructed not to enable this flag by -passing `-bypass-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. @@ -151,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 @@ -175,65 +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. - 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 +- 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 @@ -243,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: @@ -267,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 @@ -294,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 @@ -312,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 @@ -321,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 @@ -380,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 @@ -392,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: @@ -429,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 @@ -474,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 @@ -521,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). @@ -686,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). @@ -704,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 @@ -743,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 @@ -815,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 @@ -837,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 @@ -857,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 @@ -884,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 *) @@ -1002,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. @@ -1019,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 @@ -1047,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. @@ -1075,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), @@ -1089,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 @@ -1098,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. @@ -1123,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) @@ -1139,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). @@ -1169,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/xml-protocol.md b/dev/doc/xml-protocol.md index 127b4a6d2d..cf7d205d8b 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -291,7 +291,10 @@ Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ### <a name="command-status">**Status(force: bool)**</a> -CoqIDE typically sets `force` to `false`. +Returns information about the current proofs. CoqIDE typically sends this +message with `force = false` after each sentence, and with `force = true` if +the user wants to force the checking of all proofs (wheels button). In terms of +the STM API, `force` triggers a `Join`. ```html <call val="Status"><bool val="${force}"/></call> ``` |