| Age | Commit message (Collapse) | Author |
|---|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
This should ideally have been done before the 8.11 branching.
|
|
A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
flags.
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
As documented in the feedback API.
|
|
|
|
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
We cleanup a few imports on Declare, and indeed we find a suspicious
exception `AlreadyDeclared` present in `CErrors` where it should not
be there.
We move it to `Declare`, waiting for more investigation.
|
|
We place the check for unhandled exceptions in the `is_anomaly`
function, and consider all the exceptions non-handled by the printers
always anomalies.
This reworks the solution implemented in
ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular
`allow_uncaught` cannot be used anymore, all exceptions must install a
printer.
In order to pass the test-suite CI we also had to register some
printers, that were not registered for no reason, forcing clients to
call a post-processing step on errors.
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
Not sure how often this happens in practice but it seems it could.
|
|
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
This is necessary to prevent Coq from sending ill-formed output in some
scenarios involving `Timeout`.
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
|
|
This is convenient for the bootstrap of `coqdep`
|
|
|
|
As far as I understood, this was useful for tine-tuning the stm but
this is no longuer needed: it is ok not to have exception handler when
a constant registration does not span over several commands (such as
"Goal ... Qed" or obligations).
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
|
|
Instead, if the coqlib is special, we set it explicitly in the command
line, as Dune does.
This is a continuation of #9523.
In Sphinx, we stop using -boot, and pass `-coqlib` through the
environment instead.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
|
|
They didn't seem to be used at all.
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
|
|
Reviewed-by: ejgallego
|
