aboutsummaryrefslogtreecommitdiff
path: root/toplevel/stm.ml
AgeCommit message (Collapse)Author
2013-12-04The commands that initiate proofs are now in charge of what happens when ↵Arnaud Spiwack
proofs end. The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it. In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands. In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
2013-12-04Vernac classification: allow for commands which start proofs but must be ↵Arnaud Spiwack
synchrone. The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
2013-11-27STM: restart slave after every proofEnrico Tassi
The code now passes a cleanup function that, if slave is not killed, could be used to do some cleanup between two jobs. ATM I don't know how to reuse the worker without having it grow in space indefinitely. Running Gc.compact is too expensive.
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
PG sends "Set Silent" and it was messing up the DAG, making the detection of an immediate proof not working. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17061 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22STM: proper error message if the GUI edits_at a dummy stategareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16909 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22STM: do not enrich exceptions more than oncegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16908 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22STM: send the gui the status of the slavesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16899 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18Coqtop: fix looping over a broken state.gareuselesinge
Coqtop is not able to deal with broken states, hence Stm.interp has to immediately backtrack to the last meaningful state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16894 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
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
2013-10-18STM: not optimize proofs containing an Undogareuselesinge
Actually we could, but we should check the state one jumps to is inside the proof... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16889 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11STM: prefix debug messages with slave-idgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16880 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11STM: cancel slaves working on outdated jobsgareuselesinge
I did not manage to make the slave manager use Unix.select to wait for a response from the slave for a limited time and check for cancellation. Hence the following semi-cooperative model: - The slave has a thread that sends a Tick every second when the thread is working - The slave_manager will then be unblocked periodically by this tick and check for cancellation - Cancellation is, for the moment, implemented using kill. To kill a process on windows one could bind TerminateProcess (>= WinXP) or RegisterWindowMessage + BroadcastSystemMessage (>= Win2k). See: http://msdn.microsoft.com/en-us/library/windows/desktop/ms686722%28v=vs.85%29.aspx Another option is to make the slave_manager send to the tick thread on the slave process a boolean answer to the Tick message, and the tick thread could eventually bail out. But to do that, it is way better to have a second channel, used only by this tick thread. This solution sound very like the one proposed for windows, but requires more work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16878 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10STM: a proof with nested proofs cannot be delegatedgareuselesinge
The reason is that the state gets altered by side effects by the Qed of inner proofs. This kind of side effects cannot be reproduced in the slaves easily. And there is no point in working hard for this corner case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
Used by fake_ide, that before editing a broken proof has to be sure Coq known the proof is broken. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16868 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10Clib: fold_left_until added to CListgareuselesinge
CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: spit a warning if an out of bound Back* command is issuedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16859 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: understand -coq-slaves-opts extra-env=VAR=valgareuselesinge
In this way one can set an env variable for the slave, like the socket used by ocamldebug to talk remotely to a process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16844 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: if -coq-slaves off really imitate the old CoqIDEgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16843 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
STM falls back to local, lazy, evaluation if the slave dies badly or if there is a marshalling error. Both things should never occur, but is nice to have the system recover if a bug pops up. Nevertheless during regression testing these fallbacks should be disabled not to hide a new bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03Regression test suite for STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: number of slaves passed by the command linegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: avoid "kill 9 pid" if we know the slave diedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: delegate proofs to slaves only if they are not trivialgareuselesinge
Still too simple and not configurable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: take a shallow snapshot for the first proof stepgareuselesinge
this way it can be directly sent to a slave with no further manipulation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16836 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fully force a proof ourput before sending it back to the mastergareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16830 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: better error messages in case of marshal failuregareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16829 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16828 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16827 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: Unix.kill can failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16825 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: better handle proof modesgareuselesinge
Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16815 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13STM pretty printer should never failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16777 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13fix STM feeback on running jobsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16776 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Unknown commands starting a proof were not setting the proof mode.gareuselesinge
Fixes Orsay/Containers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16771 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16750 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Stm: if slave process dies badly go back to local lazy evaluationgareuselesinge
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
2013-08-30-coq-slaves: close_on_exec + correct argument passinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16742 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16704 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-12Fixing potentially misused Errors.push.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-11Mutual proofs cannot be delegatedgareuselesinge
I don't know why yet, but let's be conservative git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16697 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-10Small typosppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-10Lemmas ending with Defined cannot be delegated to slavesgareuselesinge
We need the proof object to continue (there is no real dependency tracking so we assume we need it immediately). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16694 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
This time all collateral effects of forcing the execution of dropped proofs should be handled correctly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16692 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 10:14:48 +0000