| Age | Commit message (Collapse) | Author |
|---|
|
Rewriter needs a bit of work as it calls a removed function, but no
big deal.
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
It seems to belong there, not in `tactics`
|
|
This makes sense as it is mandatory for the client.
|
|
We mark all the stuff scheduled to disappear in `Declare`, and remove
a couple of non-needed APIs.
|
|
As we are aiming to forbid low-level manipulation of proofs outside
`Declare`, we move the code from `Abstract` to `Declare`.
We remove `build_constant_by_tactic` from the public API.
|
|
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.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
|
|
|
|
|
|
Old code was doing two passes on `initial_goals`; this produced some
awkward situations code-wise.
The `~unsafe_typ` parameter to `prepare` is needed to preserve the
behavior introduced in bf0499bc507d5a39c3d5e3bf1f69191339270729 :
> Do not normalize the type of a proof according to the final universes
> when keep_body_ucst_separate is true, otherwise the type might not be
> retypable in the initial context
We need to investigate more, as of today we keep this behavior which
seems to work.
|
|
- 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`.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
|
|
As suggested by Gaëtan Gilbert.
|
|
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
|
|
|
|
|
|
After the last refactoring commit, the entry_fn function is redundant
and we can just get rid of it and get a more direct code.
|
|
We do some minor refactoring, removing one-use local definitions, and
cleaning up the `EConstr.t -> Constr.t` path, what is going on with
the use of unsafe it now becomes clear.
|
|
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
|
|
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.
|
|
We split the `close_proof` into two variants, one for delayed proof,
and one for the regular proof closing path, _à la_ interactive.
This makes sense as the typing in both cases is different, even if we
still haven't changed it.
We strongly enforce the invariant (for now) that universe polymorphic
proofs cannot be delayed using this API, as the STM expects.
It introduces some minimal, non-interesting code duplication, which
will go away in the next commits.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
|
First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.
In this first commit, we move the actual declare logic to a common
place.
|
|
|
|
|
|
|
|
We instead favor the `build_by_tactic` function which should at some
point better integrated in the declare core.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
|
|
|
|
Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
|
|
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
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`.
|
|
|
