| Age | Commit message (Collapse) | Author |
|---|
|
This allows to remove internal API from the mli as well.
|
|
Current backtraces for tactics leave a bit to desire, for example
given the program:
```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```
the backtrace stops at:
```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.
The backtrace for the failed rewrite is now:
```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
which IMO is much better.
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
|
|
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.
|
|
|
|
- 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: 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
|
|
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
This statically ensures more invariants and moves a global declaration out
of this function.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
`declare_definition` didn't improve a lot the declare path and was
used only once on interesting code. Also, it had many optional
parameters. The declare path is critical enough as to care about a
tidy API.
|
|
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
|
|
It was never used actually.
|
|
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...)
|
|
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.
We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
|
|
|
|
|
|
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
State in `Proof_global` was mostly used for debugging, so not a big
change.
|
|
Previously, they were hard-wired in the ML code.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
I think the usage looks cleaner this way.
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
