| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
It was not very useful as just parsing won't get you very far due to
lack of notation loading.
|
| |
|
|
|
|
|
|
| |
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
| |
|
|
|
|
|
| |
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
This option was not doing anything... Today, one can turn the
compatibility notations warning into an error, if ever that was the
intended semantics.
|
| | |
| |
| |
| |
| | |
These warnings can now be configured like any other, so we don't need
a specific option anymore.
|
| |/
|
|
|
|
|
|
|
|
|
| |
We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.
We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.
Test suite passes.
|
| |
|
|
|
| |
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
| |
|
|
| |
This way par:eauto and all:eato print the same debugging traecs
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
We also add a Coq86.v compat file.
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \
| | |
| | |
| | | |
Add -o option to coqc
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
This is the "error resiliency" mode for STM
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
By default we enable only {} and par: that are detectable in
a complete way.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| |\| |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Guillaume Melquiond
Pierre Letouzey
Jason Gross
Matej Kosik