aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Port g_toplevel to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
|
* [coqtop] Give priority to stdlib load path over current directoryGravatar Maxime Dénès2018-06-19
| | | | | | | | | | | | | | | | | | When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail.
* [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.
* [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.
* [toplevel] Don't ignore output filename provided by user in -oGravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | | | | | | This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447
* Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
| | | | | | | | | | The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase.
* Reporting when an error occurs at initialization time.Gravatar Hugo Herbelin2018-05-02
| | | | | | Done by simplifying the three "try" liable to be caught at initialization time into one and by ensuring that the remaining one reports about being in initialization phase.
* Merge PR #7305: [toplevel] improve indentationGravatar Emilio Jesus Gallego Arias2018-05-01
|\
| * improve indentationGravatar Enrico Tassi2018-04-23
| |
* | [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.
* [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
* [toplevel] Fix path initialization before vio processing (closes #7044)Gravatar Emilio Jesus Gallego Arias2018-04-07
| | | | | | | | | | The toplevel refactoring made path initialization per document, however vio-checking and vio-tasks are not documents, so loadpath must be initialized individually. Patch by @gares, refactoring to avoid double-initialization by me. Co-authored-by: <Enrico.Tassi@inria.fr>
* Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps ↵Gravatar Enrico Tassi2018-04-04
|\ | | | | | | with #7142]
| * [toplevel] Protect goal printing better wrt Break [fixes #7142]Gravatar Emilio Jesus Gallego Arias2018-04-01
| | | | | | | | | | | | | | | | When interrupting goal printing, we should continue the loop with the newly generated state, that should help avoiding synchronization problems as in #7142. Fixes #7142.
* | [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.
* [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.
* [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.
* Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6871: [build] Simpler byte/opt toplevel build.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \
| | | * [toplevel] Respect COQ_COLORS environment variableGravatar Thomas Hebb2018-03-07
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the toplevel."), the COQ_COLORS environment variable has been ignored, since init_terminal_output unconditionally called init_tag_map with the default colors, overwriting any custom colors that had been previously set. Fix this by creating a separate function, default_styles, to set the default colors. Also, remove the clear_styles function, as it was only called in one place and did nothing (since tag_map is empty to begin with).
* | | [toplevel] Modify printing goal strategy.Gravatar Emilio Jesus Gallego Arias2018-03-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of using a command-analysis heuristic, coqtop will now print goals if the goal has changed. We use a fast goal comparison heuristic, but a more refined strategy would be possible. This brings some [IMHO very welcome] change to PG and `-emacs`, which will now disable the printing of goals. Now, instead of playing with `Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show` command whenever it wishes to redisplay the goals. This change will break PG, so we need to carefully coordinate this PR with PG upstream (see ProofGeneral/PG#212). Some interesting further things to do: - Detect changes in nested proofs. - Uncouple the silent flag from "print goals".
| | * [build] Simpler byte/opt toplevel build.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |/ |/| | | | | | | | | | | | | | | Instead of playing static linking games, we just ship two different top-level files depending on whether we want to enable `Drop` support [bytecode case] or not. The savings of the old approach [1 line of code] were not worth the complexities of the linking hack.
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
* \ \ Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \
* \ \ \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | supported scenarios.
| | | | * | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | | |
| | | | * | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| |_|_|/ / / |/| | | | |
| | * | | | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `Drop` is implemented using exceptions-as-control flow, so the toplevel state gets corrupted as `do_vernac` will never return when `Drop` occurs in the input. The right fix would be to remove `Drop` from the vernacular and make it a toplevel-only command, but meanwhile we can just patch the state in the exception handler. We also need to keep the global state in `Coqloop` as the main `coqtop` entry point won't be called by `go ()`. Fixes #6872.
| | | * | | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | |/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We first load the file, then we print it as a post-processing step. This is both more flexible and clearer. We also refactor the comments handling to minimize the logic that is living in the Lexer. Indeed, the main API is now living in the printer, and complex interactions with the state are not possible anymore, including the removal of messing with low-level summary and state setting!
| * | | | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now.
| | * / Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ /
* / / Fix #6751 trust_file_cache logic was invertedGravatar Gaëtan Gilbert2018-02-27
|/ / | | | | | | Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
* | [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.
| * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| |
* | [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
|\
* \ Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.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] Small refactoring of fatal_error functions.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | |
| | * [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.
| * [toplevel] Disable error resiliency in `-quick` mode.Gravatar Emilio Jesus Gallego Arias2018-02-07
|/ | | | | Fixes #6707, indeed, the STM was treating some errors as recoverable thus `-quick` did succeed too often.
* [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...
* [toplevel] Refine start of interactive mode conditions.Gravatar Emilio Jesus Gallego Arias2018-02-05
| | | | | | | Refinement of the toplevel codepath requires to be more careful about the conditions for coqtop to be interactive. Fixes #6691. We also tweak the vio auxiliary function.
* [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.
* [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files *) coq_path : Names.DirPath.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = | VoPath of vo_path_spec | MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed.
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | One less global flag.