| Age | Commit message (Collapse) | Author |
|---|
|
- Mention Guillaume Claret among maintainers of the OPAM repository
(as suggested by Karl Palmskog).
- Update links to the documentation to avoid being outdated.
- Mention sections beyond the one on 8.11+beta1.
|
|
|
|
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
Use -std=c99 instead of the GCC argument -fexcess-precision=standard
This requires the -fasm as the VM is using the asm GNU extension
(also implemented by other compilers).
These flags should be more portable accross C compilers.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Latest build on SF is erroring due to:
```
"messages" : [ {
"type" : "error",
"message" : "This job has been blocked because no credits are available on your plan. Please upgrade to continue building.",
"reason" : "execution-authorization-failed"
} ],
```
we temporary pin to the last successful job that produced artifacts.
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
cons and nil
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
- What is consensus
- How to join / leave
Following suggestions from Vincent Semeriva and Maxime Dénès.
|
|
|
|
Build and install the Ltac2 documentation.
|
|
This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.
The fix here can be used for inspiration to do the make-based part.
|
|
We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.
|
|
When a newer pipeline contains the same job, the job can be
interrupted, see:
https://docs.gitlab.com/ee/ci/yaml/README.html#interruptible
This should help with job limits (c.f. #11320 )
The patch is a bit unsatisfactory due to the duplication needed;
we could define a base job and use extends, but not sure it is worth
it for now.
|
|
Reviewed-by: maximedenes
|
|
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
|
