| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Ack-by: silene
|
|
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
|
|
|
|
Reviewed-by: ejgallego
|
|
Otherwise gitlab stops logging somewhere in the middle.
Also pass -o because we can.
|
|
|
|
Reviewed-by: ejgallego
|
|
We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
|
|
- don't `set -x` while loading overlays, non-verbose untaring
- ls _build_ci to help figure out artifact download issues
|
|
|
|
|
|
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.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
|
|
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>
|
|
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
|
|
Reviewed-by: ejgallego
|
|
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.)
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
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
|
|
Reviewed-by: maximedenes
|
|
Fixes #12496
|
|
|
|
|
|
|
|
Adapted from 747936a9d9a7402f537e1e1a857c7591d8e88d2a
|
|
|
|
|
|
|
|
Following upstream advice.
|
|
1. Fix casing of build_prep_overlay argument.
Follow-up of 6cc6b87f997d7a5e848203b49bfedfaa96c53bb2
2. Call autoconf directly.
Adapted from a9996619e2d2352e0e60faf4dbde78fa1549b2af
|
|
some machines.
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
