| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
What one needs to know in 3rd party makefiles, like plugins ones,
is the Coq version and the OCaml version number. This option prints
the 2 values on a single line separated by spaces. The already existing
--version outputs the same piece of info but in a format meant for user
consumption, and hence harder to parse.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In pre 8.6, `Pp` provided its own reimplementation of
`Pervasives.flush_all`, with different semantics.
Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of
points were silently switched to the `Pervasives` version, which may
lead to some subtle printing differences.
As a preventive measure, we restore the same semantics for these parts
of the codebase.
Note that we don't re-introduce Coq's `flush_all` for several reasons:
- Consumers of the logging API should not mess with flushing and
Formatters as this is backend dependent (i.e: when in IDEs).
Use of `Format` should be fully encapsulated if we want some hope of
IDEs taking full control.
- As used, the old semantics of `flush_all` were fragile.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We revert the change of flushing strategy in the toplevel.
PR #179 introduced a different flushing in toplevel, but it creates
problems as new lines appear when Set Printing Width is large and proof
general complains, see bugzilla#4784. The use of `flush_all` also
produces missing output.
IMO, this is a pitfall of the current setup, in particular, `Format` is
used without enclosing expressions in top-level boxes, as required. This
results in undefined behavior and fragile printing such as this bug
exemplifies.
Test suite passes.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We export `Cerrors.EvaluatedError` so plugins and STM consumers can
catch it.
It took me a while to make my mind on this one, but now I am convinced
this is the right thing to do. (Another possibility is to remove
`EvaluatedError` altogether).
The rationale is as follows: when using `Stm.{add,observe}` it
will be frequent for Coq to raise a public-facing exception, however the
toplevel will wrap it into the `EvaluatedError`.
Thus, we get exceptions that we are supposed to handle, but its wrapping
in `EvaluatedError` prevents us from a more meaningful exception
handling: we are stuck with calling the printer.
In particular, this allows SerAPI/jsCoq to provide proper serialization
of most public exceptions.
|
| |\ \ \
| | | |
| | | |
| | | | |
Add -o option to coqc
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
This is the "error resiliency" mode for STM
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
non-recursive notations (#4815).
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | |_|_|_|_|_|/ /
|/| | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
By default we enable only {} and par: that are detectable in
a complete way.
|
| | |_|_|/ / / /
|/| | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
For Drop for example.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | | |
obligations".
|
| | | | | |
|
| | | | | |
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Also register properly the kind of definition.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | | |
- This patch changes the search interface to take [Str.regexp]s,
[constr_pattern]s, and [DirPath.t] instead of [string]s and
[string list]s.
- Convenience functions are provided to do the translation.
|
Hugo Herbelin
Enrico Tassi
Pierre-Marie Pédrot
Maxime Dénès
Arnaud Spiwack
Emilio Jesus Gallego Arias
Jason Gross
Matthieu Sozeau
Guillaume Melquiond
Gregory Malecha