aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
| | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* [spawn] don't create a control socket on Unix (Fix #7713)Gravatar Enrico Tassi2018-06-15
|
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | | | | | | | | | | | | | | | We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
* [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
| | | | | | | `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
* | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
* | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
| * Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
|/
* [STM] Nested Proofs Allowed has to be executed immediatelyGravatar Enrico Tassi2018-05-17
| | | | | since it affects scheduling (actually the error the option lets one silence)
* Remove deprecation warning for nested proofs.Gravatar Théo Zimmermann2018-05-17
| | | | It is not clear yet that support for nested proofs will actually get removed in a future version.
* Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
|
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | | | | | | `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
* Merge PR #7282: [toplevel] allow toploop_init change Coq optionsGravatar Emilio Jesus Gallego Arias2018-04-19
|\
| * [toplevel] let toploop_init change Coq optionsGravatar Enrico Tassi2018-04-19
| | | | | | | | | | Toplevels may want to modify for example the Stm flags, which after #1108 are handled in a functional way.
* | Merge PR #7281: [stm] push functional API furtherGravatar Emilio Jesus Gallego Arias2018-04-18
|\ \
| * | [stm] push functional API furtherGravatar Enrico Tassi2018-04-17
| |/
* / [stm] expose restore/backup since ~doc is (still) dummyGravatar Enrico Tassi2018-04-17
|/
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* [warnings] Remove `set_current_loc` hack.Gravatar Emilio Jesus Gallego Arias2018-04-11
| | | | | | | | | | Instead of the current hack that won't work as soon as we check some part of the document asynchronously, we make the warning processor recover a proper location if the warning doesn't have one attached. This is what CoqIDE does [but it queries it's own document model]. Fixes: #6172
* Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Gravatar Enrico Tassi2018-04-05
|\
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
* \ \ Merge PR #7132: [doc] Add some more documentation to STM API.Gravatar Enrico Tassi2018-04-01
|\ \ \
| | | * [stm] More cleanup of "classification is not an interpreter"Gravatar Emilio Jesus Gallego Arias2018-04-01
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove meta-information from the query classification and we don't process `Stm.query` as a transaction anymore, as the right API is available to it to execute the command directly. This simplifies pure commands and removes some impossible cases. Depends on #7138.
| | * [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
| | | | | | | | | | | | | | | | | | This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack.
| * | [doc] Add some more documentation to STM API.Gravatar Emilio Jesus Gallego Arias2018-03-31
| |/
* / Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/
* stm: don't propagate side effects when editing a proofGravatar Enrico Tassi2018-03-27
|
* Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Enrico Tassi2018-03-26
|\
| * [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
| | | | | | | | | | | | This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
* | [stm] Never consider `Backtrack` as part of the script.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/ | | | | | | | | This makes Emacs's `Backtrack` commands to be similar to `EditAt`, thus they will correctly revert the document state. This fixes #6240 and likely some other synchronization bugs. It is still unfortunate that true meta commands are part of the vernacular, we should fix this for 8.9.
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | | | | The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
* Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
|
* 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
| |