| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
Enrico Tassi