| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: maximedenes
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
Recent changes in Coqbot plus the unfortunate breakage OCaml upstream
has make this too noisy.
We will re-enable once https://github.com/ocaml/dune/pull/3585
is accepted upstream.
|
|
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
|
|
Reviewed-by: ejgallego
|
|
Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.
|
|
We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.
Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.
|
|
definitions
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Apparently the `Timeout` exception is raised by a signal handled, and
that can happen when the running thread is a worker manager, rather than
the main thread (the one that should be interrupted).
Given that the point of these tests is to test *auto and not the STM,
we disable async proofs forcibly.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
|
|
I used SYSMOD from Makefile.build as the ground truth.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
|
|
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.
|
