aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofworkertop.ml
Commit message (Collapse)AuthorAge
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| | | | | | We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
* [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | We mostly separate command line argument parsing from interpretation, some (minor) imperative actions are still done at argument parsing time. This tidies up the code quite a bit and allows to better follow the complicated command line handling code. To this effect, we group the key actions to be performed by the toplevel into a new record type. There is still room to improve.
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | 4.02.3 has been the minimal OCaml version for a while now.
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [stm] Add common toploop for workers.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | This is a small, but convenient refactoring, as it will allow common argument parsing.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* STM: code refactoringGravatar Enrico Tassi2014-11-03
| | | | | This is mainly shuffling code around and removing internal refs that are not needed anymore.
* STM: reorganize code and file namesGravatar Enrico Tassi2014-10-31
- proofworkertop to deal with proof tasks - tacworkertop to deal with par: tactics - queryworkertop to deal with queries (next commit)