| Age | Commit message (Collapse) | Author |
|---|
|
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
|
|
|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
|
|
|
|
vernac
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]
This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.
Logic could be pushed upwards, but this is good enough for now.
This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.
The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .
|
|
It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.
Considering that I think it's fair enough to remove it.
|
|
This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.
The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.
We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.
Fixes #3632 #3890 #4638.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
This arose after a question by Talia Ringer on how to log
user-interaction with a Coq document.
The hooks would allow a plugin to receive events about user data.
This is experimental and will need some tweaks to be useful for sure,
in particular w.r.t. errors.
[Note: this is safe enough as to be included in 8.9]
|
|
not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
This has been a mess for quite a while, we try to improve it.
|
|
|
|
We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
|
|
This is a fairly small cleanup on the `vernac_interp` function, which
makes code cleaner and for example would allow to have `Load` inside
`Load`. [Not that we would ever want that]
|
|
We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.
|
|
|
|
Fixes #8320
|
|
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
|
|
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
Reviewed-by: ejgallego
|
|
This makes the implementation of Timeout on unix more reliable
since only the main thread will receive the signal for
timeout.
|
|
This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.
|
|
|
|
|
|
|
|
|
|
|
|
proofs.
We forbid commands that may open proofs inside proofs.
|
|
Since some state handling refactoring, `purify_stm` was no longer
protecting against assignement of cur_id, resulting in confusing
behavior w.r.t. cache.
|
|
(fix #9204)
|
|
|
|
workers
|
