| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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).
|
|
Let proof terms are stocked in the named_context that is used directly
everywhere, hence there is no way to stock a Future proof term there.
|
|
|
|
|
|
the flag with_conv_pbs, only reset the metas, not the last_mod field. It seemed
strange to mix two unrelated things. This did not break anything visible...
|
|
|
|
Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.
This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.
Much of this could be reused for the VM.
|
|
|
|
|
|
The sharing introduced by this commit is now correct, since a reference used by
the native compiler has been removed from constant_body.
This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.
|
|
For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
|
|
Also, the future chain that reaches the kernel is greedy.
If the user executes step by step, then the error is raised immediately.
|
|
To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
|
|
|
|
If a Future.computation is already a value v or an exception and
is chained in a greedy way with a function f, then f v is executed
immediately (or the exception is raised).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
when internalizing a term.
|
|
internalization time.
|
|
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
|
|
|
|
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
and nia.
|
|
|
|
interpreter.
|
|
|
|
It triggered nonsensical behaviour of list-using tactic
notation. Hopefully or not, nobody uses such notations out of
the test-suite...
|
|
|
|
|
|
|
|
Attempt to adapt .el files too.
doc/refman/RefMan-uti.tex has still to be fixed.
|
|
|
|
test-suite pass.
|
|
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
|
|
If these messages are still relevent to somebody, feel free to
restore them in -debug or any non-default mode of your choice.
|
|
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
|
