| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
|
|
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.
This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.
Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
|
|
We make the types of the delayed / non-delayed declaration path
different, as the latter is just creating futures that are forced
right away.
TTBOMK the new code should behave identically w.r.t. old one, modulo
the equation `Future.(force (from_val x)) = x`.
There are some questions as what the code is doing, but in this PR
I've opted to keep the code 100% faithful to the original one, unless
I did a mistake.
|
|
This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
|
|
`wits` is actually not used, it is set in equations to the list of
evars corresponding to the goals.
|
|
The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook
We handle this automatically now; it seems like a reasonably good API
improvement.
However, it is not clear what we do now is right for all cases; must
check.
|
|
This is a step in forcing all entry creation go thru the preparation
functions. We still need to handle plain `Declare.` calls, but this
will be next step.
We need to leave a backdoor for interactive proofs until we unify
proof preparation happening in `Proof_global` with the one happening
in `DeclareDef`, but we are getting there.
TODO: see how to avoid the normalization problems in DeclareObl
|
|
This is a tiny step towards making the code closer to its counterpart
in `DeclareDef`.
|
|
In previous versions of Coq `abstract` could create non-uniform bodies
for mutually recursive definitions (c.f. bug #5065)
Thanks to changes to the trusted base this is not the case anymore,
thus we can remove the workaround.
This way mutual bodies are handled the same in the interactive and
non-interactive case.
|
|
This gets us closer to the code in `DeclareDef` for the
non-interactive case.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
|
This could still use some more work due to the way proofs are
structured, in particular:
- the handling of the primary type w.r.t. Econstr
- refining Info.t so open/close invariants hold by typing
Very interestingly, better typing means that the tension between
tension between `start_dependent_lemma` and the handling of mutual
definitions starts to surface.
In particular, the information contained in `Info.thms` is not to be
used by all non-standard terminators.
However, it seems that such refactoring would better fit once we have
finished cleaning up the regular save path.
|
|
Steps towards unification with `DeclareDef` API.
|
|
Steps towards unification with `DeclareDef` API.
|
|
We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.
This is the last step before unifying both paths.
|
|
|
|
|
|
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
Add headers to a few files which were missing them.
|
|
Now that `MutualEntry` provides a more uniform interface we can reuse
`Info.t`
In the medium term we shall consolidate `Proof` / `Proof_global` and
`Lemmas` so admitted / finish are uniform too.
|
|
We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.
This should be almost semantically equivalent to the previous code,
including some questionable choices present there.
In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
|
|
As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
|
|
We move towards more unification in the proof save path of interactive
and non-interactive proofs.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
This means return_proof is the only place where it can be produced.
We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.
I'm not sure if this works correctly though, how to test?
We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.
Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a
|
|
Reviewed-by: ejgallego
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
|
|
This lets us remove the closure passing for the program inference_hook
|
|
|
|
Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.
This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.
So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.
To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.
|
|
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
|
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
|
|
This lets us remove the passing around of "status" in comassumption
and generally makes highlighting axiom adding lines in coqide more
reliable as there's no need for per-command code.
If a command adds multiple axioms it will emit AddedAxiom multiple
times, this doesn't seem to be a problem though.
We may wonder if "Fail Fail Axiom" should be highlighted as
"Axiom" (both before and after this commit it is).
|
|
We make the interface to this function simpler, as a step towards
trying to remove the duplication of this function with the code in
`DeclareDef`.
|
