diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-20 18:02:19 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-04 17:07:15 +0100 |
| commit | ecda2159a3c3176fb871bbc27b7c6b56d9f0830c (patch) | |
| tree | 8fa3a8ae6f9bb5cf8378cd9c8752fd0cffa94885 /tools/coqc.ml | |
| parent | 2541662136c24a209dbbd71366aa77788120434f (diff) | |
.vi files: .vo files without proofs
File format:
The .vo file format changed:
- after the magic number there are 3 segments. A segment is made of 3
components: bynary int, an ocaml value, a digest. The binary int
is the position of the digest, so that one can skip the value without
unmarshalling it
- the first segment is the library, as before
- the second segment is the STM task list
- the third segment is the opaque table, as before
A .vo file has a complete opaque table (all proof terms are there).
A .vi file follows the same format of a .vo file, but some entries
in the opaque table are missing. A proof task is stocked instead.
Utilities:
coqc: option -quick generates a .vi insted of a .vo
coq_makefile: target quick to generate all .vi
coqdep: generate deps for .vi files too
votour: can browse .vi files too, the first question is which segment
should be read
coqchk: rejects .vi files
Diffstat (limited to 'tools/coqc.ml')
| -rw-r--r-- | tools/coqc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index 89ab64b67..3b01f90c4 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -117,7 +117,7 @@ let parse_args () = |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" - |"-impredicative-set"|"-vm"|"-no-native-compiler" + |"-impredicative-set"|"-vm"|"-no-native-compiler"|"-quick" |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem -> parse (cfiles,o::args) rem |