| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
When initilazing the load path, coqtop adds implicit bindings for stdlib
and for the current directory (-R stdlib Coq -R . ""). In case of
a clash, the binding of the current directory had priority, which makes
it impossible to edit stdlib files (when they Require files from the
same directory) using PG, or from CoqIDE when launched from the directory
containing the file.
Example to reproduce the problem:
```
cd plugins/omega
coqide Omega.v
```
some of the Requires will fail.
|
|
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
|
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
|
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
|
This was a silly bug introduced in
675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly
forward the command line option.
Thanks to @SkySkimmer for finding out the problem.
closes #7447
|
|
The five phases are command line interpretation, initialization,
prelude loading, rcfile loading, and sentence interpretation (only the
two latters are located).
We then parameterize the feedback handler with the given execution
phase, so as to possibly annotate the message with information
pertaining to the phase.
|
|
Done by simplifying the three "try" liable to be caught at
initialization time into one and by ensuring that the remaining one
reports about being in initialization phase.
|
|
|
|
|
|
Toplevels may want to modify for example the Stm flags,
which after #1108 are handled in a functional way.
|
|
Instead of the current hack that won't work as soon as we check some
part of the document asynchronously, we make the warning processor
recover a proper location if the warning doesn't have one attached.
This is what CoqIDE does [but it queries it's own document model].
Fixes: #6172
|
|
The toplevel refactoring made path initialization per document,
however vio-checking and vio-tasks are not documents, so loadpath must
be initialized individually.
Patch by @gares, refactoring to avoid double-initialization by me.
Co-authored-by: <Enrico.Tassi@inria.fr>
|
|
with #7142]
|
|
When interrupting goal printing, we should continue the loop with the
newly generated state, that should help avoiding synchronization
problems as in #7142.
Fixes #7142.
|
|
This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.
|
|
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
|
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.
|
|
|
|
|
|
|
|
Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the
toplevel."), the COQ_COLORS environment variable has been ignored,
since init_terminal_output unconditionally called init_tag_map with
the default colors, overwriting any custom colors that had been
previously set. Fix this by creating a separate function,
default_styles, to set the default colors.
Also, remove the clear_styles function, as it was only called in one
place and did nothing (since tag_map is empty to begin with).
|
|
Instead of using a command-analysis heuristic, coqtop will now print
goals if the goal has changed. We use a fast goal comparison
heuristic, but a more refined strategy would be possible.
This brings some [IMHO very welcome] change to PG and `-emacs`, which
will now disable the printing of goals. Now, instead of playing with
`Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show`
command whenever it wishes to redisplay the goals.
This change will break PG, so we need to carefully coordinate this PR
with PG upstream (see ProofGeneral/PG#212).
Some interesting further things to do:
- Detect changes in nested proofs.
- Uncouple the silent flag from "print goals".
|
|
Instead of playing static linking games, we just ship two different
top-level files depending on whether we want to enable `Drop` support
[bytecode case] or not.
The savings of the old approach [1 line of code] were not worth the
complexities of the linking hack.
|
|
|
|
|
|
|
|
|
|
supported scenarios.
|
|
|
|
|
|
`Drop` is implemented using exceptions-as-control flow, so the
toplevel state gets corrupted as `do_vernac` will never return when
`Drop` occurs in the input.
The right fix would be to remove `Drop` from the vernacular and make
it a toplevel-only command, but meanwhile we can just patch the state
in the exception handler.
We also need to keep the global state in `Coqloop` as the main
`coqtop` entry point won't be called by `go ()`.
Fixes #6872.
|
|
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
|
|
Parsing in `VernacLoad` was broken for a while, but the situation has
improved by miscellaneous refactoring.
However, we still cannot support `Load` properly when proofs are
crossing file boundaries. So in this patch we do two things:
- We check for supported scenarios [no proofs open at `Load` entry/exit]
- Remove the hack in `toplevel` so the behavior of `Load` is
consistent between `coqide`/`coqc`.
We close #5053 as its main bug was fixed by the main toplevel
refactoring and the remaining cases are documented now.
|
|
|
|
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
|
|
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
|
|
|
|
|
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
|
|
|
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
|
|
Fixes #6707, indeed, the STM was treating some errors as recoverable
thus `-quick` did succeed too often.
|
|
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...
|
|
Refinement of the toplevel codepath requires to be more careful about
the conditions for coqtop to be interactive.
Fixes #6691. We also tweak the vio auxiliary function.
|
|
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.
|
|
We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.
To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:
```
type add_ml = AddNoML | AddTopML | AddRecML
type vo_path_spec = {
unix_path : string; (* Filesystem path contaning vo/ml files *)
coq_path : Names.DirPath.t; (* Coq prefix for the path *)
implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
}
type coq_path_spec =
| VoPath of vo_path_spec
| MlPath of string
type coq_path = {
path_spec: coq_path_spec;
recursive: bool;
}
```
Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.
This API is necessarily internal [for now] thus I don't think a
changes entry is needed.
|
