| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
md5sum check remains not portable.
|
|
|
|
|
|
Thanks again Maximes.
This time the C value was stored in the env_(named|rel)_val of
the environment
|
|
considered files.
Original patch by Guillaume Allais.
|
|
|
|
|
|
|
|
|
|
Kudos to Maximes for finding the culprit in no time!
Values of type 'Pre_env.key' store in the OCaml state the 'address'
of an already evaluated constant in the VM's C state. Such values
are not sent to work processes. The worker is going to re-evaluate the
constant, but just once, since the cache is cleared only when the env is
marshalled (via ephemerons).
|
|
|
|
|
|
without"
This reverts commit bfe1141026da70d8f59cf47b5fe61ffc20a29f3c.
Conflicts:
proofs/proofview_monad.ml
This is potentially a temporary commit until a final decision is taken on hand-written versus extracted ocaml for the tactic monad. The hand-written implementation has a bug where the + tactical would not behave properly (I tried to find why, but couldn't: the hand-written implementation looks fine, but it isn't. Beats me).
There is a conflict with Pierre-Marie's commit 4832692: Fixing backtrace registering of various tactic-related try-with blocks.
|
|
|
|
|
|
Proof using can be followed by:
- All : all variables
- Type : all variables occurring in the type
- expr:
- (a b .. c) : set
- expr + expr : set union
- expr - expr : set difference
- -expr : set complement (All - expr)
Exceptions:
- a singleton set can be written without parentheses. This also allows
the implementation of named sets sharing the same name space of
section hyps ans write
- bla - x : where bla is defined as (a b .. x y) elsewhere.
- if expr is just a set, then parentheses can be omitted
This module also implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.
Finally, one can Set Default Proof Using "str" to any string that is
used whenever the "using ..." part is missing. The coding of this
sucks a little since it is the parser that applies the default.
|
|
|
|
It is not possible to add shortcuts with arbitrary modifiers and to
save into a state some data, like the line offset for C-n and the
killed text for C-k and C-y.
If you see that your favorite Emacs/PG shortcut is missing,
please tell me!
Currently supported shortcuts:
C-_ Undo
C-g Esc
C-s Search
C-e Move to end of line
M-e Move to end of sentence
M-a Move to beginning of sentence
C-n Move to next line
C-p Move to previous line
C-f Forward char
C-b Backward char
M-f Forward word
M-b Backward word
C-k Kill untill the end of line
M-d Kill next word
M-k Kill until sentence end
M-DELBACK Kill word before cursor
C-d Delete next character
C-y Yank killed text back
C-c C-RET Go to
C-c C-n Advance 1 sentence
C-c C-u Retract 1 sentence
C-c C-b Advance
C-c C-r Restart
C-c C-c Stop
C-c C-a C-p Print
C-c C-a C-c Check
C-c C-a C-b About
C-c C-a C-a Search About
C-c C-a C-o Search Pattern
C-c C-a C-l Locate
C-c C-a C-RET match template
C-x C-s Save
C-x C-c Quit
C-x C-f Open
|
|
The original idea was to send not the kernel name, but the file/line
to that CoqIDE could make the text an hyperlink to the file, exactly
as coqdoc generated HTML.
|
|
|
|
|
|
-async-proofs off
the system behaves as in 8.4
-async-proofs lazy
proofs are delayed (when possible) but never processed in parallel
-async-proofs on
proofs are processed in parallel (when possible). The number of
workers is 1, can be changed with -async-proofs-j. Extra options to
the worker process can be given with -async-proofs-worker-flags.
The default for batch compilation used to be "lazy", now it is "off".
The "lazy" default was there to test the machinery, but it makes very
little sense in a batch scenario. If you process things sequentially,
you'd better do them immediately instead of accumulating everything in
memory until the end of the file and only then force all lazy computations.
The default for -ideslave was and still is "on". It becomes dynamically
"lazy" on a per task (proof) basis if the worker dies badly.
Note that by passing "-async-proofs on" to coqc one can produce a .vo
exploiting multiple workers. But this is rarely profitable given
that master-to-worker communication is inefficient (i.e. it really
depends on the size of proofs v.s. size of system state).
|
|
|
|
The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.
The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.
This user interface is still very rough, it should probably run the
workers instead of just printing their command line.
|
|
|
|
|
|
If a proof has no "Proof using" but we are building a .vi and
the aux file contains such piece of info, we use it to process
the proof asynchronously.
|
|
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
|
|
|
|
The default action is to raise NotReady, but one may want to
make the action "blocking" but successful. Using this device
all delayed proofs can be "delegated". If there are slaves, they
will eventually pick up the task. If there are no slaves, then
the future can behave like a regular, non delegated, lazy computation.
|
|
This has nothing to do with the kernel itself, but it is
the place where this piece of data is inferred.
|
|
|
|
|
|
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).
|
