| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
packaging
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
beta versions.
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
No reason to have them in the same .sh
|
|
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
|
|
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2,
only with the pinned version, and bedrock2 is still relatively unstable.
So we make the CI not have Fiat-Crypto depend on bedrock2, and instead
use the pinned submodule, by using `EXTERNAL_REWRITER=1
EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
The computation of which files to build is now mostly cached rather than
computed, eliminting basically all of the wait-time from `make` to the
first invocation of `coqc`.
Note that we no longer need to invoke
`./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds
up `coqdep` somewhat significantly.
Fixes #9298
|
|
Reviewed-by: maximedenes
|
|
|
|
* Add hyperlinks
|
|
Reviewed-by: ppedrot
|
|
Also, stop pinging when copying checklist to new issue.
|
|
|
|
This is necessary until we get of the voboot step.
See https://github.com/coq/coq/pull/11406#issuecomment-577261843 for
more details.
|
|
|
|
|
|
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
|
|
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
|
|
|
|
|
|
We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.
|
|
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
...
```
|
|
This brings dune at version 2.1.2
|
|
|
|
|
|
Reviewed-by: JasonGross
|
|
|
|
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
|
|
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
Integrate merging doc in the main contributing document.
|
|
Reviewed-by: ejgallego
|
|
- remove manual flexlink circular dependency handling
- use standard configure process instead of hand made windows make files
- enable parallel build
- remove bootstrapping step (maybe should be there for release builds)
|
