aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [stm] Partial fix for bug #6884 [location missing from replay nodes]Gravatar Emilio Jesus Gallego Arias2018-03-02
| | | | | | | | | | | | | | | | | | | | | | | | Example not yet fixed by this patch: ``` Definition u : Type. Definition m : Type. exact nat. Defined. exact bool. Defined. ```
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* [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.
* Merge PR #6693: [toplevel] Refactor command line argument handling.Gravatar Maxime Dénès2018-02-13
|\
* | [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | | | | | | The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
| * [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.
* Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\
* \ Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵Gravatar Maxime Dénès2018-02-05
|\ \ | | | | | | | | | VernacDefinition
| | * [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc...
| * [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
| |
| * [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
| |
* | [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
|/ | | | | | | | We gather (almost) all the STM options in a record, now set at document creation time. This is refactoring is convenient for some other ongoing functionalization work.
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
| * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
| |
* | Fix mli-doc issue #6531Gravatar Tony Beta Lambda2018-01-01
|/
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | One less global flag.
* Merge PR #6318: Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-22
|\
| * Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | | | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* | [stm] [ide protocol] Allow to include several commands on query.Gravatar Emilio Jesus Gallego Arias2017-12-16
|/ | | | This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
* Merge PR #1108: [stm] Reorganize flagsGravatar Maxime Dénès2017-12-13
|\
* \ Merge PR #6275: [summary] Allow typed projections from global state.Gravatar Maxime Dénès2017-12-12
|\ \
| | * [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | | | | | | | | | | | | | | | | | | | | We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
| | * [stm] Move process_id to Spawned.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |/ |/| | | | | | | This brings us one step closer to actually moving all STM flags to `stm`.
* | [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | | | | | | | Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
| * [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ | | | | | We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively.
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* Merge PR #6233: [proof] [api] Rename proof types in preparation for ↵Gravatar Maxime Dénès2017-12-01
|\ | | | | | | functionalization.
* | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | | | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
| * [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
|/ | | | | In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
* [vernac] Adjust `interp` to pass polymorphic in the attributes.Gravatar Emilio Jesus Gallego Arias2017-11-27
|
* Merge PR #6207: [stm] Allow delayed constant in interactive mode.Gravatar Maxime Dénès2017-11-27
|\
* \ Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueueGravatar Maxime Dénès2017-11-23
|\ \
| * | [stm] [doc] Add some documentation to AsyncTaskQueue APIGravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | | | | | As a bonus we remove some trailing whitespace, and implement a couple of hints suggested in the discussion.
* | | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ / | | | | | | | | | | | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
| * [stm] Allow delayed constant in interactive mode.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ | | | | | | | This setting is a debug assertion, due to the many flags we still over-approximate setting the flag to true to all interactive environments. [So the assert is checked in vo compilation] Fixes #6152.
* Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\
* \ Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \
| | * [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/| | | | | | | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
| * Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
| | | | | | | | Fixes #6165.
* | [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | This is a first step towards some of the solutions proposed in #6008.
* 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] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
* [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | We still don't thread the state there, but this is a start of the needed infrastructure.
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away.
* [stm] First step to move interpretation of Undo commands out of the classifier.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself.
* Merge PR #1103: Take Suggest Proof Using outside the kernel.Gravatar Maxime Dénès2017-10-13
|\