aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* [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.
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface.
* [coqtop] Don't reset coqinit internal variables after initialization.Gravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | We remove `init_library_roots` as there is no point in resetting this internal variable. Its only user is `init_load_path` and this function is not meant (and is not) idempotent now.
* Merge PR #1069: Improve support for -w optionsGravatar Maxime Dénès2017-10-05
|\
* \ Merge PR #1106: Fix beautifierGravatar Maxime Dénès2017-10-05
|\ \
| * | Remove catch-all try with in the beautifier.Gravatar Théo Zimmermann2017-09-27
| | |
| * | Beautifier gets its own formatter: fixes BZ#5704.Gravatar Théo Zimmermann2017-09-27
| | |
* | | [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
|/ / | | | | | | | | | | | | Undo & friends is very expensive in batch mode as backtracking state is not kept and thus should be recomputed. We thus warn the user.
* | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \
* \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \
| * | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| | | |
| | | * Handle multiple -w options on command line (bug #5736).Gravatar Guillaume Melquiond2017-09-21
| | |/ | |/|
* / | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/ / | | | | | | | | | | | | | | | | | | | | An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info`
| * Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
|
* Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Gravatar Maxime Dénès2017-08-29
|\
* | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| | | | | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
* | Merge PR #917: Moving --print-version to -print-version for consistency.Gravatar Maxime Dénès2017-08-01
|\ \
| | * [general] Remove spurious dependency of highparsing on toplevel.Gravatar Emilio Jesus Gallego Arias2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | `G_vernac` was depending on `toplevel` just for parsing the compat number information. IMHO this was not the right place, so I have moved the parsing bits to parsing and updated the files. This allows to finally separate the `toplevel` from Coq, which avoids linking it in alternative toplevels.
* | | [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ |/| | | | | Minor clean up, no sense in having these as they do nothing.
* | Merge PR #902: Only perform profile initialization and printing when the ↵Gravatar Maxime Dénès2017-07-26
|\ \ | | | | | | | | | flag is set.
| | * Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25
| | |
* | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |/ |/|
| * Also a less intrusive Profile.init_profile.Gravatar Hugo Herbelin2017-07-20
|/ | | | | | Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible.
* Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
| | | | | | | | This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* "There are pending proofs" error message now lists the name of the proofs.Gravatar Théo Zimmermann2017-06-16
| | | | This closes https://coq.inria.fr/bugs/show_bug.cgi?id=5275
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#758: [toplevel] Print error header on fatal batch error.Gravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \
| | | * Add support for Coq 8.6.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | | * Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | | * Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | | * Add a version to be used when parsing compatibility notations mentioning old ↵Gravatar Guillaume Melquiond2017-06-14
| |_|/ |/| | | | | | | | versions.
* | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
| * | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
|/ / | | | | | | | | | | | | | | | | As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`.
| * [toplevel] Print error header on fatal batch error.Gravatar Emilio Jesus Gallego Arias2017-06-10
|/
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | Document --print-version in UsageGravatar Enrico Tassi2017-05-23
| | | |
| | * | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | and avoid duplication
| | * | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| |/ /
| * | Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Maxime Dénès2017-05-20
| |\ \
| * \ \ Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Gravatar Maxime Dénès2017-05-20
| |\ \ \
| | | | * [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | |_|/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 11:27:26 +0000