| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.
In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.
Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
|
|
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
|
|
|
|
Now that the interface has mostly stabilized, we move code around to
respect internal dependency order.
This will allow us to start sharing more code in the 4 principal
cases, and also paves the way for the full merging of obligations and
the removal of the Proof_ending type in favor of stronger type
abstraction.
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
|
|
|
|
This removes so ad-hoc tuples, and encapsulates the API a bit.
It is a step towards:
- Pushing some `to_constr` from the upper layers to the declare code
itself [which will remove code duplication, in particular making the
interactive / non-interactive path more uniform, and make the API
easier to use]
- Further refactoring of the constant information, as `Recthm.t`
contains almost now what we would call "primitive constant
information"; thus we will be able to distinguish next better between
mutual declarations and single-constant ones.
|
|
When declaring a lemma, the code path is quite different depending on
whether the lemma is inferred to be a mutually-defined lemma or not.
We refactor the code path in declare to reflect that; this will allow
to better organize constant information and to reuse the `Recthm.t`
type in particular.
|
|
|
|
|
|
|
|
|
|
Step towards merging `Info / `CInfo`; the presentation order is now
"final" in the sense of that we propose this API for the medium-term.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
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.
|
|
This hides even more internals; we will reduce the API even more
shortly.
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.
|
|
We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
It makes sense to require it to be uni-goal; this also removes some
duplication.
See the caveat with the handling of `~sign` tho.
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
|
|
|
|
|
|
Fixes #12582
The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should
be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says
that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime
`plik.v.log` is older than `Nat.vo`. This is circular, and results in
`make` considering all of the `modules/` tests out-of-date on any fresh
run.
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
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.)
|
|
They were deprecated in 8.12.
|
|
No need to return the list of generated evars, this was never used.
|
|
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
All calls to this function are now factorized through Clenvtac.res_pf.
|
|
|
|
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
Reviewed-by: mattam82
|
|
This reverts commit b35030760cadd96a968e04f3cd026f4abdc0331c.
|
|
Reviewed-by: SkySkimmer
|
|
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.)
|
|
Fixes #12571.
|
|
Reviewed-by: MSoegtropIMC
Ack-by: SkySkimmer
|
|
Reviewed-by: gares
Reviewed-by: maximedenes
|
