aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.ml
Commit message (Collapse)AuthorAge
* Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08
|
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
| | | | | | 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.
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | 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.
* Future: API for blocking futuresGravatar Enrico Tassi2014-11-28
|
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
|
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
| | | | | | | | | | | | | | 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
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
| | | | the checker, and it was not used before that anyway.
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
| | | | | | | 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.
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
|
* Future: better error messageGravatar Enrico Tassi2014-05-15
|
* Future: memory optimization when forcing a chained pure computationGravatar Enrico Tassi2014-04-25
| | | | Kudos to PMP for spotting that!
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | 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.
* Future: make ~greedy:true the default + new sink commodity APIGravatar Enrico Tassi2014-02-26
|
* Future: each computation has a uuidGravatar Enrico Tassi2014-02-26
|
* STM: fix valid_id coming from Qed errorsGravatar Enrico Tassi2014-02-10
|
* fix typoGravatar Enrico Tassi2014-01-06
|
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | -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).
* Future: allow custom action when a delegated future is forcedGravatar Enrico Tassi2014-01-04
| | | | | | | | 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.
* Future: optional greedy chainingGravatar Enrico Tassi2013-12-24
| | | | | | 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).
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
| | | | | | | | | | | 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
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
| | | | | | | | | | | | | | | | 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
* lib/future: computations that are Exn can be replacedGravatar gareuselesinge2013-09-30
| | | | | | | | 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
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
| | | | | | | | 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 Conv_oracle state for type checkingGravatar gareuselesinge2013-08-30
| | | | | | | 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
* Stm: if slave process dies badly go back to local lazy evaluationGravatar gareuselesinge2013-08-30
| | | | | | | | | | | 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
* Fixing potentially misused Errors.push.Gravatar ppedrot2013-08-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small typosGravatar ppedrot2013-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
* checker validation fixed w.r.t. FuturesGravatar gareuselesinge2013-08-09
| | | | | | | 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
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
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