| Age | Commit message (Collapse) | Author |
|---|
|
As far as I understood, this was useful for tine-tuning the stm but
this is no longuer needed: it is ok not to have exception handler when
a constant registration does not span over several commands (such as
"Goal ... Qed" or obligations).
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.
Consequently, `Vernacentries.interp` takes a state, and returns the
new one.
We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.
I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.
In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:
- master:
real 2m11,027s
user 8m30,904s
sys 1m0,000s
- no_futures:
real 2m8,474s
user 8m34,380s
sys 0m59,156s
|
|
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
|
|
The current future system is lazy when "chaining" (*) a resolved
future, which implies that chaining with a resolved future will produce
a non-resolved one.
This misfeature interacts badly with the "purification" optimization,
which in turn provokes a swarm of spurious state setting calls in real
use.
To solve this problem, we revert to the more natural semantics of
respecting the evaluation semantics when mapping over a future, indeed
respecting the previous resolution status.
This commit solves a kind of _critical_ bug in the current system,
with the particular bad path origination in `Future.split2` due to the
following accumulation of circumstances:
```
split2 x -> chain x (fun x -> fst x)
=>
let y = chain ~pure x (fun x -> fst x) in
if is_over x && greedy then ignore(force ~pure y);
y
=> [y <- Closure (fun x -> fst x)]
ignore(force (Closure (fun x -> fst x)))
=>
purify_future (force ~pure) (Closure (fun x -> fst x))
```
and then, the test in `purify_future` fails, triggering the
spurious state reset operation.
This problem was first noted at
https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and
seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382
We fix the problem by making chaining eager, but other solutions would
be possible. Given that the main user of `chain` is `split2` which
does `snd/fst`, I recommend this solution.
The difference in calls to `unfreeze_state` is dramatic:
```
| File | Freeze Calls After | Freeze Calls Before |
|----------------------------------------+--------------------+---------------------|
| theories/Init/Notations.v | 0 | 0 |
| theories/Init/Logic.v | 57 | 614 |
| theories/Init/Datatypes.v | 13 | 132 |
| theories/Init/Logic_Type.v | 7 | 57 |
| theories/Init/Specif.v | 5 | 35 |
| theories/Init/Nat.v | 0 | 0 |
| theories/Init/Peano.v | 22 | 264 |
| theories/Init/Wf.v | 8 | 89 |
| theories/Init/Tactics.v | 2 | 24 |
| theories/Init/Tauto.v | 0 | 0 |
| theories/Init/Prelude.v | 0 | 0 |
| Bool/Bool.v | 104 | 1220 |
| Program/Basics.v | 0 | 0 |
| Classes/Init.v | 0 | 0 |
| Program/Tactics.v | 0 | 0 |
| Relations/Relation_Definitions.v | 0 | 0 |
| Classes/RelationClasses.v | 21 | 341 |
| Classes/Morphisms.v | 47 | 689 |
| Classes/CRelationClasses.v | 18 | 245 |
| Classes/CMorphisms.v | 50 | 587 |
| Classes/Morphisms_Prop.v | 3 | 127 |
| Classes/Equivalence.v | 6 | 105 |
| Classes/SetoidTactics.v | 0 | 0 |
| Setoids/Setoid.v | 4 | 33 |
| Structures/Equalities.v | 8 | 93 |
| Relations/Relation_Operators.v | 0 | 0 |
| Relations/Operators_Properties.v | 35 | 627 |
| Relations/Relations.v | 2 | 24 |
| Structures/Orders.v | 12 | 148 |
| Numbers/NumPrelude.v | 0 | 0 |
| Structures/OrdersTac.v | 13 | 234 |
| Structures/OrdersFacts.v | 73 | 931 |
| Structures/GenericMinMax.v | 82 | 1294 |
| Numbers/NatInt/NZAxioms.v | 0 | 0 |
| Numbers/NatInt/NZBase.v | 7 | 87 |
| Numbers/NatInt/NZAdd.v | 14 | 168 |
| Numbers/NatInt/NZMul.v | 12 | 144 |
| Logic/Decidable.v | 28 | 336 |
| Numbers/NatInt/NZOrder.v | 81 | 1174 |
| Numbers/NatInt/NZAddOrder.v | 24 | 288 |
| Numbers/NatInt/NZMulOrder.v | 46 | 552 |
| Numbers/NatInt/NZParity.v | 35 | 420 |
| Numbers/NatInt/NZPow.v | 29 | 348 |
| Numbers/NatInt/NZSqrt.v | 54 | 673 |
| Numbers/NatInt/NZLog.v | 64 | 797 |
| Numbers/NatInt/NZDiv.v | 49 | 588 |
| Numbers/NatInt/NZGcd.v | 36 | 432 |
| Numbers/NatInt/NZBits.v | 0 | 0 |
| Numbers/Natural/Abstract/NAxioms.v | 0 | 0 |
| Numbers/NatInt/NZProperties.v | 0 | 0 |
| Numbers/Natural/Abstract/NBase.v | 14 | 177 |
| Numbers/Natural/Abstract/NAdd.v | 6 | 72 |
| Numbers/Natural/Abstract/NOrder.v | 29 | 349 |
| Numbers/Natural/Abstract/NAddOrder.v | 5 | 60 |
| Numbers/Natural/Abstract/NMulOrder.v | 8 | 96 |
| Numbers/Natural/Abstract/NSub.v | 36 | 432 |
| Numbers/Natural/Abstract/NMaxMin.v | 18 | 216 |
| Numbers/Natural/Abstract/NParity.v | 4 | 48 |
| Numbers/Natural/Abstract/NPow.v | 26 | 312 |
| Numbers/Natural/Abstract/NSqrt.v | 9 | 108 |
| Numbers/Natural/Abstract/NLog.v | 0 | 0 |
| Numbers/Natural/Abstract/NDiv.v | 50 | 600 |
| Numbers/Natural/Abstract/NGcd.v | 14 | 168 |
| Numbers/Natural/Abstract/NLcm.v | 29 | 348 |
| Numbers/Natural/Abstract/NBits.v | 168 | 2016 |
| Numbers/Natural/Abstract/NProperties.v | 0 | 0 |
| Arith/PeanoNat.v | 77 | 990 |
| Arith/Le.v | 2 | 57 |
| Arith/Lt.v | 14 | 168 |
| Arith/Plus.v | 20 | 269 |
| Arith/Gt.v | 17 | 248 |
| Arith/Minus.v | 11 | 132 |
| Arith/Mult.v | 14 | 168 |
| Arith/Between.v | 19 | 299 |
| Logic/EqdepFacts.v | 26 | 539 |
| Logic/Eqdep_dec.v | 13 | 361 |
| Arith/Peano_dec.v | 3 | 26 |
| Arith/Compare_dec.v | 35 | 360 |
| Arith/Factorial.v | 3 | 36 |
| Arith/EqNat.v | 10 | 111 |
| Arith/Wf_nat.v | 18 | 173 |
| Arith/Arith_base.v | 0 | 0 |
| Numbers/BinNums.v | 0 | 0 |
| PArith/BinPosDef.v | 0 | 0 |
| PArith/BinPos.v | 229 | 2810 |
| NArith/BinNatDef.v | 0 | 0 |
| NArith/BinNat.v | 107 | 1330 |
| PArith/Pnat.v | 51 | 688 |
| NArith/Nnat.v | 30 | 360 |
| setoid_ring/Ring_theory.v | 43 | 756 |
| Lists/List.v | 195 | 2908 |
| setoid_ring/BinList.v | 6 | 90 |
| Numbers/Integer/Abstract/ZAxioms.v | 0 | 0 |
| Numbers/Integer/Abstract/ZBase.v | 3 | 36 |
| Numbers/Integer/Abstract/ZAdd.v | 46 | 552 |
| Numbers/Integer/Abstract/ZMul.v | 8 | 96 |
| Numbers/Integer/Abstract/ZLt.v | 21 | 252 |
| Numbers/Integer/Abstract/ZAddOrder.v | 45 | 543 |
| Numbers/Integer/Abstract/ZMulOrder.v | 24 | 288 |
| Numbers/Integer/Abstract/ZMaxMin.v | 22 | 264 |
| Numbers/Integer/Abstract/ZSgnAbs.v | 41 | 492 |
| Numbers/Integer/Abstract/ZParity.v | 6 | 72 |
| Numbers/Integer/Abstract/ZPow.v | 10 | 120 |
| Numbers/Integer/Abstract/ZDivTrunc.v | 68 | 816 |
| Numbers/Integer/Abstract/ZDivFloor.v | 70 | 840 |
| Numbers/Integer/Abstract/ZGcd.v | 29 | 348 |
| Numbers/Integer/Abstract/ZLcm.v | 50 | 600 |
| Numbers/Integer/Abstract/ZBits.v | 205 | 2460 |
| Numbers/Integer/Abstract/ZProperties.v | 0 | 0 |
| ZArith/BinIntDef.v | 0 | 0 |
| ZArith/BinInt.v | 212 | 2839 |
|----------------------------------------+--------------------+---------------------|
```
(*) I would call it `Future.map` better than chain.
|
|
It was always set to `greedy:true`.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
|
|
|
|
|
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
|
|
|
|
|
|
|
|
This makes queries like Print or Extraction block and not
raise the error "the value is not ready". This should make
CoqIDE work for every kind of script.
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
|
|
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
the checker, and it was not used before that anyway.
|
|
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
|
|
|
|
|
|
Kudos to PMP for spotting that!
|
|
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
|
|
|
|
|
|
|
|
-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 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.
|
|
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).
|
|
This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored. This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A computation that is an exception morally holds no value
hence can be replaced by an type-equivalent computation.
This mechanism is used to edit broken proofs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The Stm commit switched from an home made handling of failures to
a with_state_protection. This was wrong, since in case of success
the global state has to be left altered.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
safe_typing is not purely functional, hence we cannot chain it
as if it was a pure computation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Processing the proof in a slave process may fail for an implementation
error, e.g. the state could not be marshalled, or an anomaly is raised
by the slave.
In this case we fall back to local, lazy, evaluation in the master
process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
still not working, it complains about the universe constraint
set...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures.
Futures can represent local (lazy) computations or remote ones
(delegated). Delegating a future lets a third party assign its
value at some poit in the future; in the meanwhile accessing the
future value raises an exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
|
