aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* 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
| |
| * 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.
* | Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵Gravatar Maxime Dénès2017-12-27
|\ \ | | | | | | | | | possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
| | * [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | | | | | One less global flag.
* | | [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
| * Forbidding -o and -f in input file of coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | This was apparently either silently doing nothing or failing.
* | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \
* \ \ Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \ \
* \ \ \ Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ \ \ \ | | | | | | | | | | | | | | | same right-hand side.
* \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1108: [stm] Reorganize flagsGravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ \
| | | | | | * | [lib] Auxiliary functions in List + fixes.Gravatar Emilio Jesus Gallego Arias2017-12-13
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | These are convenient to use `command.ml` for example. We also fix a critical bug in the `fold_left_map` family of functions, as witnessed by this old behavior. ```ocaml fold_left2_map (fun c u v -> c+1,u+v) 0 [1;2;3] [1;2;3;];; - : int * int list = (3, [6; 4; 2]) ``` I have opted for a simple fix keeping the tail-recursive nature, I am not in the mood of writing base libraries, but feel free to improve.
| | | | * | | Improving spacing in printing disjunctive patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Adding a space before the bar separating disjunctive patterns. Removing an extra space after the bar for inner disjunctive patterns.
| | | * | | | Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| | | |/ / / | | | | | | | | | | | | | | | | | | And some code simplification.
| * | | | | [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`.
| | * | | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
| | * | | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |/ / / | | | | | | | | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* / / / [lib] Convenience function for `Dyn.Easy`Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ / /
* | | Rename update to set, fixes #6196Gravatar Paul Steckler2017-12-05
| | |
| * | [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
* | Merge PR #6241: [lib] Generalize Control.timeout type.Gravatar Maxime Dénès2017-11-27
|\ \
| * | [lib] Generalize Control.timeout type.Gravatar Emilio Jesus Gallego Arias2017-11-24
| | | | | | | | | | | | | | | We also remove some internal implementation details from the mli file, there due historical reasons.
* | | Unify style of comments in file CUnix.Gravatar Hugo Herbelin2017-11-23
| | |
* | | Add a function to surround filenames containing a space with quotes.Gravatar Hugo Herbelin2017-11-23
|/ /
* | [lib] Minor pending cleanup to consolidate helper function.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | While we are at it we refactor a few special cases of the helper.
* | Merge PR #6117: Fix printing anomaly in convGravatar Maxime Dénès2017-11-13
|\ \ | |/ |/|
* | Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Gravatar Maxime Dénès2017-11-08
|\ \
| | * Fixing an (apparently misplaced) spc in anomaly reporting message.Gravatar Hugo Herbelin2017-11-08
| | |
| * | [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
| |/
* / [feedback] Helper to print feedback messages in the console.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/ | | | | This is useful for tools such as `coqchk` or `coq_makefile` that want to handle feedback on their own.
* Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Maxime Dénès2017-11-03
|\
* | Naming the type of Dyn.Map for future reuse.Gravatar Hugo Herbelin2017-11-02
| |
| * 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.