aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Util.Empty: implement using polymorphic record.Gravatar Gaëtan Gilbert2018-07-03
|
* CWarnings.normalize_flags: removed unused ~silent argument.Gravatar Gaëtan Gilbert2018-07-03
|
* [envars] honor env variable COQLIBGravatar Enrico Tassi2018-07-02
|
* Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Gravatar Emilio Jesus Gallego Arias2018-06-28
|\
* | Slightly less crazy parsing algorithm for CoqProject_file.Gravatar Pierre-Marie Pédrot2018-06-27
| | | | | | | | | | We use a buffer instead of O(n) appending to a string, and we also make the parser tail-call.
* | Turn CoqProject_file into a normal OCaml file.Gravatar Pierre-Marie Pédrot2018-06-27
| |
| * Fix #7704: get_toplevel_path needs normalised argv.(0)Gravatar Gaëtan Gilbert2018-06-22
|/ | | | | | | | | | When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.
* [spawn] don't create a control socket on Unix (Fix #7713)Gravatar Enrico Tassi2018-06-15
|
* Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ | | | | | | in CArray
* | Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.Gravatar Théo Zimmermann2018-05-24
| |
| * Moving Rtree.smart_map into Rtree.Smart.map.Gravatar Hugo Herbelin2018-05-23
| |
| * Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
|/
* [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.
* Merge PR #7437: [coqdep] Minor cleanups.Gravatar Pierre-Marie Pédrot2018-05-10
|\
| * [CoqProject] Add some comments and remove unnecessary use of Pp.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | | | | | | But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
* | [lib] Re-add `set_timeout` to help users workaround #7408Gravatar Emilio Jesus Gallego Arias2018-05-07
|/ | | | | | It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment.
* Merge PR #6958: [lib] Move global options to their proper place.Gravatar Maxime Dénès2018-04-30
|\
* | Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
* | Merge PR #7194: [warnings] Remove `set_current_loc` hack.Gravatar Maxime Dénès2018-04-12
|\ \
* \ \ Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac ↵Gravatar Pierre-Marie Pédrot2018-04-12
|\ \ \ | | | | | | | | | | | | failure in other file
| | * | [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
| * | Fixing #7100 (lost of main file location in case of Ltac failure in other file).Gravatar Hugo Herbelin2018-04-04
| | |
| | * [lib] Move global options to their proper place.Gravatar Emilio Jesus Gallego Arias2018-04-02
| | | | | | | | | | | | | | | | | | | | | | | | Recent commits introduced global flags, but these should be module-specific so relocating. Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced to the truly global stuff.
* | | Fix #7101: STM delegation policy brokenGravatar Maxime Dénès2018-03-28
| |/ |/| | | | | | | I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel.
* | [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.
* Merge PR #6496: Generate typed generic code from ltac macrosGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Gravatar Maxime Dénès2018-03-09
|\ \ | | | | | | | | | fiat-crypto/OSX
| | * Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| |/ |/| | | | | | | | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
| * Closes #6830: coqdep reads options and files from _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | Note that we don't look inside -arg for eg -coqlib.
* | Remove non-existent dependencyGravatar mrmr19932018-03-05
| |
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
* | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | |
* | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| | |
| | * Add source (project file / command line) to project fields.Gravatar Gaëtan Gilbert2018-03-01
| | |
| | * Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSXGravatar Gaëtan Gilbert2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix as suggested by @JasonGross by reading file names from the _CoqProject when coq_makefile was invoked with one. I made coqdep only look at the .v files from _CoqProject because it's easier this way. Since we're going through the _CoqProject parser we could have coqdep understand more of it but let's leave that to another PR (and maybe someone else). Some projects pass vfiles on the command line, we keep the list of these files to pass them to coqdep via command line even when there is a _CoqProject. Multiple project files is probably broken.
| * | 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
* New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
* Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ | | | | | | | | | camlp4
| * | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | longer use camlp4.
| | * [ide] Localize a IDE-specific flag.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |/ |/|
* | [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].
* [lib] Respect change of options under with/without_option.Gravatar Emilio Jesus Gallego Arias2018-01-30
| | | | | | | | | | | | | | | | | | | The old semantics of `with/without_option` allowed the called function to modify the value of the option. This is an issue mainly with the `silently/verbose` combinators, as `Set Silent` can be executed under one of them and thus the modification will be lost in the updated code introduced in a554519874c15d0a790082e5f15f3dc2419c6c38 IMHO these kind of semantics are quite messy but we have to preserve them in order for the `Silent` system to work. In fact, note that in the previous code, `with_options` was not consistent with `with_option` [maybe that got me confused?] Ideally we could restore the saner semantics once we clean up the `Silent` system [that is, we remove the flag altogether], but that'll have to wait. Fixes #6645.
* Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\
* \ Merge PR #6405: Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-29
|\ \
* \ \ Merge PR #6433: [flags] Move global time flag into an attribute.Gravatar Maxime Dénès2017-12-29
|\ \ \
| | | * [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| |_|/ |/| | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
| | * Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
| |/ |/| | | | | | | | | Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it.