| 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 .
|
|
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
|
|
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
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).
For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.
Incidentally, this avoids the non-recommended Loadpath.locate_file.
|
|
|
|
This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
|
|
|
|
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.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
TODO coqproject handling (for now it can be done through -arg I guess)
|
|
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
|
|
|
|
We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
This is necessary to prevent Coq from sending ill-formed output in some
scenarios involving `Timeout`.
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
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
|
|
Reviewed-by: gares
|
|
|
|
|
|
This fixes #9484 .
|
|
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
|
