| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
since it affects scheduling (actually the error the option lets one
silence)
|
| |
|
|
| |
It is not clear yet that support for nested proofs will actually get removed in a future version.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
|
|
| |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
| |
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
| |
We remove meta-information from the query classification and we don't
process `Stm.query` as a transaction anymore, as the right API is
available to it to execute the command directly.
This simplifies pure commands and removes some impossible cases.
Depends on #7138.
|
| |
|
|
|
|
| |
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.
|
| |/
|
|
|
|
|
|
|
| |
This makes Emacs's `Backtrack` commands to be similar to `EditAt`,
thus they will correctly revert the document state. This fixes #6240
and likely some other synchronization bugs.
It is still unfortunate that true meta commands are part of the
vernacular, we should fix this for 8.9.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Example not yet fixed by this patch:
```
Definition u : Type.
Definition m : Type.
exact nat.
Defined.
exact bool.
Defined.
```
|
| |/ |
|
| |
|
|
|
|
|
|
|
| |
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].
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
VernacDefinition
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| |
|
|
| |
One less global flag.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
| |
This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
This brings us one step closer to actually moving all STM flags to
`stm`.
|
| |/
|
|
|
|
| |
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
|
| |
|
|
|
| |
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
As a bonus we remove some trailing whitespace, and implement a couple
of hints suggested in the discussion.
|
Benjamin Barenblat
Pierre-Marie Pédrot
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Gaëtan Gilbert
Vincent Laporte