aboutsummaryrefslogtreecommitdiff
path: root/toplevel/stm.ml
AgeCommit message (Expand)Author
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-12-04Vernac classification: allow for commands which start proofs but must be sync...Arnaud Spiwack
2013-11-27STM: restart slave after every proofEnrico Tassi
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-22STM: proper error message if the GUI edits_at a dummy stategareuselesinge
2013-10-22STM: do not enrich exceptions more than oncegareuselesinge
2013-10-22STM: send the gui the status of the slavesgareuselesinge
2013-10-18Coqtop: fix looping over a broken state.gareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18STM: not optimize proofs containing an Undogareuselesinge
2013-10-11STM: prefix debug messages with slave-idgareuselesinge
2013-10-11STM: cancel slaves working on outdated jobsgareuselesinge
2013-10-10STM: a proof with nested proofs cannot be delegatedgareuselesinge
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-10Clib: fold_left_until added to CListgareuselesinge
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
2013-10-07STM: spit a warning if an out of bound Back* command is issuedgareuselesinge
2013-10-03STM: understand -coq-slaves-opts extra-env=VAR=valgareuselesinge
2013-10-03STM: if -coq-slaves off really imitate the old CoqIDEgareuselesinge
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
2013-10-03Regression test suite for STMgareuselesinge
2013-10-03STM: number of slaves passed by the command linegareuselesinge
2013-10-03STM: avoid "kill 9 pid" if we know the slave diedgareuselesinge
2013-10-03STM: delegate proofs to slaves only if they are not trivialgareuselesinge
2013-10-03STM: take a shallow snapshot for the first proof stepgareuselesinge
2013-10-01STM: fully force a proof ourput before sending it back to the mastergareuselesinge
2013-10-01STM: better error messages in case of marshal failuregareuselesinge
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
2013-10-01STM: Unix.kill can failgareuselesinge
2013-09-30STM: better handle proof modesgareuselesinge
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-13STM pretty printer should never failgareuselesinge
2013-09-13fix STM feeback on running jobsgareuselesinge
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
2013-09-12Unknown commands starting a proof were not setting the proof mode.gareuselesinge
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
2013-08-30Stm: if slave process dies badly go back to local lazy evaluationgareuselesinge
2013-08-30-coq-slaves: close_on_exec + correct argument passinggareuselesinge
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
2013-08-12Fixing potentially misused Errors.push.ppedrot
2013-08-11Mutual proofs cannot be delegatedgareuselesinge
2013-08-10Small typosppedrot
2013-08-10Lemmas ending with Defined cannot be delegated to slavesgareuselesinge
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 05:24:21 +0000