| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
|
|
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.
|
|
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
|
|
Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.
This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
|
|
|
|
When opening a file without extension, an uncaught exception was
occurring.
Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
|
|
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
|
|
Add -o option to coqc
|
|
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
|
|
|
|
|
|
|
|
Stm used to delegate every proof when it was possible, but this may
be a bad idea. Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).
Now it delegates only proofs that take >= 1 second.
By default a proof takes 1 second (that may be wrong).
If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.
After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).
CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.
|
|
|
|
|
|
For a file dir/a.v the corresponding aux file dir/.a.aux can store
arbitrary data. It maps a "Loc.t * string" (key) to a "string" (value).
Pretty much anything can fit in this schema, but ATM I see only the
following possible uses:
1) record inferred data, like the set of section variable used, so that
one can later use this info to process proofs asynchronously (i.e.
compute their discharged type without knowing the proof term).
2) record timings (how long it takes to build a proof term or check it),
so that one can take smarter scheduling decisions
3) record a bloated proof trace for automatic tactics, so that one can
replay it faster (a sort of cache). For that to be useful an Ltac
API is required.
The .aux file contains the path of the .v and its md5 hash. When loaded
it defaults to the empty map is the file is not there or if the .v file
changed.
Not finding some data in the .aux file cannot be a failure, but finding
it may help in many ways.
The current file format is very simple but human readable. It is
generated/parsed using printf/scanf and in particular the %S formatter
for the value string. The file format is private to the Aux_file
module: only an abstract interface is provided.
The current file format is not robust in face of local changes.
Any change invalidates the md5 hash (and the Loc.t is very likely to
change too).
|
