aboutsummaryrefslogtreecommitdiff
path: root/toplevel/stm.ml
AgeCommit message (Expand)Author
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-02STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Enrico Tassi
2014-03-26STM: when an error occurs in a worker send back a bunch of statesEnrico Tassi
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-04STM: fix Show ScriptEnrico Tassi
2014-03-04STM: when finish a task hcons universe constraintsEnrico Tassi
2014-02-26STM: better debug messagesEnrico Tassi
2014-02-26STM: do not print goals on UndoEnrico Tassi
2014-02-26STM: better messages when checking/finishing tasksEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26STM: backup/restore remote countersEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-10STM: when a worker is canceled mark the proof as brokenEnrico Tassi
2014-02-10STM: be conservative w.r.t. proofs containing global side effectsEnrico Tassi
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30STM: worker sends back to master the last valid stateEnrico Tassi
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-26STM: ported to spawnEnrico Tassi
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-14STM: fix -async-proofs lazyEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-07typosEnrico Tassi
2014-01-06STM: handle side effects of workers correctlyEnrico Tassi
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05STM: fix error messages while in batch mode (closes: 3196)Enrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04STM: use sec vars in aux file if no Proof using when building .viEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2014-01-04STM: simple refactoringEnrico Tassi
2014-01-04STM: set loc for aux file when interpreting vernacEnrico Tassi
2014-01-04STM: record in aux file proof build and check timeEnrico Tassi
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-12-24cleanup warningEnrico Tassi
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-12-04Stm: remove an assertion.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 02:28:31 +0000