| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #3907: CoqIDE File->Revert all buffers does not work.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We don't need to handle `Dynlink` errors specially anymore.
|
|
This should allow digest-based builds to work correctly.
Fixes #10874
For now, we store the digest of the module selected, this means that
vo files loading modules will have different digests depending on
whether the `native` or `byte` version was used.
If that is a problem we can improve this tho; for example we could
disable the digest in those cases.
The code could be better, and indeed `Mltop` could enjoy a nice
cleanup, I will likely do some when I add support for `Fl_dynload`.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
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
...
```
|
|
|
|
preparation for direct discharge
|
|
|
|
|
|
This brings dune at version 2.1.2
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: anton-trunov
Reviewed-by: herbelin
|
|
decorations
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Fixes #10909: Set Default Proof Mode is not documented.
|
|
OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.
We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).
Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.
Fix #10495
|
|
type of h.
Reviewed-by: ppedrot
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
The type of h is reconstructed to look as much as the initial type of
h as possible.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
commands"
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification. This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.
|
|
|
