aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/aux_file.ml
Commit message (Collapse)AuthorAge
* Fix #7101: STM delegation policy brokenGravatar Maxime Dénès2018-03-28
| | | | | 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.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | Now it is a private field, locations are optional.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\
| * Fix broken .aux machinery.Gravatar Guillaume Melquiond2017-01-13
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Avoid using the deprecated Scanf.fscanf function.Gravatar Maxime Dénès2017-01-09
|/
* Fix #5183 - Two CoqIDE crash errorsGravatar Maxime Dénès2016-11-30
| | | | | | | | | | 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!).
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ | | | | | | Add -o option to coqc
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/ | | | | | | | | | | | | | | | 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
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
| | | | | | | | | | | | | | | | | | | | 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.
* amending last commitGravatar Enrico Tassi2014-02-27
|
* better warningGravatar Enrico Tassi2014-02-27
|
* Aux_file: cache information at compile time for later (re)useGravatar Enrico Tassi2014-01-04
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).