| Age | Commit message (Collapse) | Author |
|---|
|
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
This will ensure that we don't introduce problems as it has happened
in the past.
While we are at it, we fix one easy case of non-tail call.
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
|
|
Add headers to a few files which were missing them.
|
|
We refactor handling of `-boot` so the "coqlib" guessing routine,
`Envars.coqlib ()` is not called when bootstrapping.
In compositional builds involving Coq's prelude we don't want for this
guessing to happen, as the heuristics to locate the prelude will fail
due to different build layout choices.
Thus after this patch Coq does not do any guessing when `-boot` is
passed, leaving the location of libraries to the usual command line
parameters.
Note that some other tooling still calls `Envars.coqlib`, however this
should happen late enough as for it to be safe; we will fix that
eventually when we consolidate the library for library handling among
tools.
Ideally, we would also remove `Envars.coqlib` altogether, as we want
to avoid clients accessing the Coq filesystem in a non-controlled way.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
In previous refactorings `vernac_loop` stopped being tail-recursive,
we refactor code a bit and make it back into tail-recursive form.
|
|
We refactor control loop a bit to make the code more readable:
- the code for unhandled exception is not needed anymore as it cannot
happen.
- we move the processing of toplevel commands to its own function
- we split away diff-specific functions.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Close #10918
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
|
|
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
|
|
We place control attributes on their own, datatype, similarly to
regular attributes.
This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
|
|
|
|
It has been deprecated since 8.4. The documentation was incorrect since
at least 8.5 (the last two arguments were ignored).
`Backtrack m n p` was a synonym for `BackTo m`
We also move `BackTo` handling to coqtop, since it is not meant to be
part of the document.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
|
|
It prints a goal given its internal goal id and the Stm state id.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
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.
|
|
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.
|
|
|
|
This uses a new coqtop-only option "Coqtop Exit On Error", not sure where
to put the doc for it. It being an option means we can locally turn it
off (.. coqtop:: fail).
|
|
This was dead code, it was never raised ever.
|
|
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>
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
|
|
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
This is localized version of #8833, but instead of adding a phase
attribute which, as pointed by @gares has some problematic semantics,
we add a local one to the toplevel functions.
This moves the imperative part of the API to a better-delimited scope
and allows to progress with the separation of the interactive and
compilation API.
Note that still quite a few issues do remain in the "Feedback" path,
for example, idetop and other feedback clients cannot get a hold of
the feedback early enough as to direct init messages to the IDE part.
This is for example a serious issue of the API that shall be treated
separately.
|
|
|
|
in 7d2a9df
(current code always prints context, should print only if the proof has changed).
Bug fix: Fix message that came out as "Error: Error: -diffs requires ..."
Enhancement: always print the context after the "Set Diffs" command.
|
|
|
|
Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.
Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm. A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.
Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
"-diffs on|off|removed" on the OS command line. The "on" option shows only the
new item with added text, while "removed" shows each modified item twice--once
with the old value showing removed text and once with the new value showing
added text.
The highlights use 4 tags to specify the color and underline/strikeout.
These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".
The first two are for added or removed text; the last two are for
unmodified parts of a modified item.
Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and
"end.diff.*", but only on the first and last strings of the span.
|
|
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 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.
|
|
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.
|
