| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
| |
|
|
|
|
|
|
| |
We gather (almost) all the STM options in a record, now set at
document creation time.
This is refactoring is convenient for some other ongoing
functionalization work.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
| |
|
|
|
|
|
|
| |
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
| |
|
|
|
|
|
|
| |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
| |
|
|
|
| |
We still don't thread the state there, but this is a start of the
needed infrastructure.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
| | |
|
| |
|
|
|
|
|
|
| |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| |\ |
|
| | | |
|
| |/
|
|
| |
Now it is a private field, locations are optional.
|
| |
|
|
|
|
|
|
|
|
|
| |
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.
This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.
This commit supersedes PR#204.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
|
| |
|
|
|
| |
`process_error_hook` seems unnecesary, we just call the proper error
interpretation.
|
| |
|
|
|
| |
`tactic_being_run_hook` was used for the "xml" pluging but I am not
sure we have a sensible use case here.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
We extend `Stm.vernac_interp` so it can handle the commands it should
by level. This reenables `Show Script` handling, and this
interpretation function should handle more commands in the future such
as Load.
However note that we must first refactor the parsing state handling a
bit and remove the legacy `Stm.interp` before that.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |
|
|
|
|
|
|
|
|
| |
PR#173 introduced a record field name clash in `stm.mli`, with duplicate
fields `start/stop` for the types `focus` and `static_block_declaration`.
We fix by renaming the younger ones (as to minimize code
incompatibilities), but other options are possible/could be preferred,
however they would be quite more invasive so I think they should be
postponed for the day the Stm API is cleaned up.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.
Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).
Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.
|
| |
|
|
|
|
|
|
|
| |
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
|
| | |
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
| |
involving Futures.
|
| |
|
|
| |
PIDEtop needs these to implement its new transaction mechanism
|
| |
|
|
|
| |
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Thanks the the previous patchset a worker can be asked to send
back "light" version of the system states. This is reasonably
efficient hence the idea of letting a worker hang around just to
hold system states for retrieval on demand is dropped.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
| |
|
|
| |
Even indirectly, if it depends on another state that in turn failed.
|
| | |
|
| |
|
|
|
|
|
|
| |
When async_proofs_always_delegate is on, park proof workers and
dispatch to them queries. This flips the current way of printing
goals in PIDE base UIs: it is not the worker that prints all goals
while coomputing the states (and the dies), it is the UI that asks
for them when they are under the eyes of the user.
|
| |
|
|
| |
The default hook value is the one used by CoqIDE
|
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Maxime Dénès
Gaetan Gilbert
Matej Kosik
Matthieu Sozeau
Alec Faithfull