| Age | Commit message (Collapse) | Author |
|---|
|
main path
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: gares
|
|
We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.
Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.
|
|
It is completely local to that file, there was no point to put it into
the unrelated Declare file.
|
|
It was never used actually.
|
|
|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
|
|
theorems.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
with coqtop
Reviewed-by: gares
Ack-by: jfehrle
|
|
Reviewed-by: vbgl
|
|
As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
|
|
Followup on "[api] Remove `polymorphic` type alias, use labels instead."
|
|
|
|
These are only needed when closing / admitting a proof.
|
|
|
|
|
|
This seems like the right location, a bit more refactoring should be
possible.
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
|
|
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
|
|
This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.
There are more cases like this, like `poly`, all are covered by
subsequent commits.
|
|
|
|
Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
|
|
|
|
Information about interactive mutually recursive proofs was stored as
a closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
TODO: Should investigate what's going on with implicits, maybe submit
a separate PR.
|
|
Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
We prepare to put the information about rec_thms in the state too.
|
|
Reviewed-by: ejgallego
|
|
It was always the negation of the opacity flag.
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
|
|
|
|
|
|
Even more invariants can be enforced this way.
|
|
|
