| Age | Commit message (Collapse) | Author |
|---|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
The current `perf` CI target is quite heavy, failing from out of
memory sometimes. We use the target suggested by Jason Gross (<- thanks)
in https://github.com/coq/coq/pull/12577#issuecomment-651970064
|
|
|
|
|
|
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca.
(I've not added back the nix things, since I'm not sure what purpose
they serve, and I've adjusted the targets slightly.)
The CI build should no longer take an enormously long time to start, and
fiat-crypto-legacy code is actively being used to track down memory
issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825,
and so I'd like to keep f-c-l in the CI at least until #7825 is
finished.
I've been maintaining compatibility of f-c-l with master anyway on the
side, in part to continue some performance experiments with it, and
expect to continue to do so at least until the end of this calendar
year, and it'd be nice for me to get advance warning when a PR is going
to break it on master. (It seems reasonable to me to take it off the CI
again once I'm no longer maintaining it / collecting data from it, and /
or once #7825 is finished.)
|
|
It's tested on the bench, so might as well test it on the CI. Hopefully
it's not too memory-heavy. (It should only take a couple of minutes,
time-wise.)
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
Following upstream advice.
|
|
some machines.
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
Note that this should reduce the overall build time of fiat-crypto
related targets by about 10--20 minutes, as I've removed the heaviest
jobs (about 25--30 minutes in serial) from the OCaml target.
I'd like to keep the OCaml target around just to make sure that Coq
doesn't introduce a change to extraction that breaks compilation of
extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826
for the issue tracking performance of compiling the extracted OCaml
code (and perhaps there should be another issue opened on the OCaml bug
tracker about flambda on the fiat-crypto extracted files?)
Alternative to #12405
Closes #12405
Fixes #12400
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
This is a new development where I'm aggregating a specific set of
benchmarks. It's intended to be relatively lightweight, taking only a
handful of minutes. It's probably one of the few developments currently
testing Ltac2.
|
|
cc: #12350
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
|
|
- use a different mirror for main cygwin archive
- (always) publish build log as artifact
- fix call to dune makefiles
- we do just build Coq for now, as:
+ dune is rebuilding Coq to run the test-suite, this needs move
investigation.
+ the test suite seems to take long and it times-out on Win.
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
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...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
We move from the previous complex CI download setup to a much more
straightforward public mirror repository.
Thanks to Yishuai Li and Benjamin Pierce for the very quick response.
Closes #12290
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: gares
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
