| Age | Commit message (Collapse) | Author |
|---|
|
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 use a buffer instead of O(n) appending to a string, and we also
make the parser tail-call.
|
|
|
|
When launched through PATH argv.(0) is just the command name.
eg "coqtop -compile foo.v" -> argv.(0) = "coqtop"
Using executable_name also follows symlinks but this isn't tested to
avoid messing with windows. Running Coq through a symlink is not as
important as PATH anyways.
|
|
|
|
in CArray
|
|
|
|
|
|
|
|
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.
|
|
|
|
But indeed we need to split this file, as it is used now from CoqIDE
is incorrect.
|
|
It seems like #7408 will need some potentially intrusive work, so
let's add the low-level hook back so third party developments can work
well with `8.8.1/master` for the moment.
|
|
|
|
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
|
|
|
failure in other file
|
|
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
|
|
|
|
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
|
|
I make here a minimal fix, but a lot of cleaning should be done around
Aux_file handling, including removing some code from the kernel.
|
|
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.
|
|
|
|
fiat-crypto/OSX
|
|
Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.
PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.
|
|
Note that we don't look inside -arg for eg -coqlib.
|
|
|
|
|
|
|
|
|
|
|
|
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
|
|
|
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
|
|
This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.
This code was written by Benjamin Grégoire and myself.
|
|
|
|
camlp4
|
|
longer use camlp4.
|
|
|
|
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].
|
|
The old semantics of `with/without_option` allowed the called function
to modify the value of the option. This is an issue mainly with the
`silently/verbose` combinators, as `Set Silent` can be executed under
one of them and thus the modification will be lost in the updated code
introduced in a554519874c15d0a790082e5f15f3dc2419c6c38
IMHO these kind of semantics are quite messy but we have to preserve
them in order for the `Silent` system to work. In fact, note that in
the previous code, `with_options` was not consistent with
`with_option` [maybe that got me confused?]
Ideally we could restore the saner semantics once we clean up the
`Silent` system [that is, we remove the flag altogether], but that'll
have to wait.
Fixes #6645.
|
|
|
|
|
|
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
