| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
We do not have to increase the step counter when out of the threaded mode since
this counter is only relevant when in that mode.
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
We try to avoid reallocating the map in two different ways.
- We only add a value when actually needed.
- We compute the union of maps with the first element as a starting point.
|
|
A set was created only to be folded over. Since the list is ensured to
be duplicate-free, there is no point in creating the former, we just
fold over the list directly.
|
|
|
|
In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.
However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.
Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.
This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.
We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.
This has been tested in the case that tactics succeed but Qed fails
asynchronously.
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
We tweak the message a bit.
|
|
|
|
|
|
|
|
See CEP#44 for futher details.
|
|
This is useful as witnessed by #11829 , as some errors printers do
still fail, so it costs little to have both backtraces.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
|
|
Reviewed-by: ppedrot
|
|
This is only used in `Ccalgo` and it does not provide any advantage
these days over the upstream OCaml implementation.
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
Reviewed-by: ppedrot
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
|
|
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
|
|
As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .
In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.
Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.
We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.
Closes #6446
Example with backtrace from https://github.com/coq/coq/issues/11366
Old:
```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
New:
```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
|
|
Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
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.
|
|
|
