| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
After #12504 , we can encapsulate and consolidate low-level state
logic in `Vernacstate`, removing `States` which is now a stub.
There is hope to clean up some stuff regarding the handling of
low-level proof state, by moving both `Evarutil.meta_counter` and
`Evd.evar_counter_summary` into the proof state itself [obligations
state is taken care in #11836] , but this will take some time.
|
|
|
|
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
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 is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
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.
|
|
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.
|
|
Error happened only when writing:
functional induction f x y z.
instead of
functional induction (f x y z).
Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
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...
|
|
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
|
|
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
|
|
|
|
This function was used almost everywhere with the wrapper around.
|
|
|
|
(incidentally fixes #7697)
Reviewed-by: Lysxia
|
|
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
|
|
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.
|
|
Reviewed-by: Matafou
Ack-by: Zimmi48
Ack-by: maximedenes
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
As part of the proof refactoring work I am doing some modifications to
`funind` and indentation of that code is driving me a bit crazy; I'd
much prefer to delegate it to an automatic tool.
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
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`.
|
|
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
|
|
Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.
Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.
This PR is in preparation for that.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).
We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
|
|
Add headers to a few files which were missing them.
|
|
Fixes #11846: Funind fails to generate principles for terms with let bindings.
|
|
|
