aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* | 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.
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
* Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ↵Gravatar Maxime Dénès2017-10-12
|\ | | | | | | STM (BZ#5556)
| * [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | | We move delicate library/module instillation code to the STM so the API guarantees that the first state snapshot is correct. That was not the case in the past, which meant that the STM cache was unsound in batch mode, however we never used its contents due to not backtracking to the first state. This provides quite an improvement in the API, however more work is needed until the codepath is fully polished. This is a critical step towards handling the STM functionally.
* | Restoring test on ident validity while browsing directory structure.Gravatar Hugo Herbelin2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | The test was abandoned at the time of merging subdirectory browsing between coqdep and coqtop, and to limit at the same time the dependency of coqdep in files such as unicode.cmo. But checking ident validity speeds up browsing in arbitrary directory structure and we restore it for this reason. (One could also say that browsing arbitrary directory structures is not intended, but in practice this may happen, as e.g. reported in BZ#5734.)
* | Adding headers to segmenttree.{ml,mli}.Gravatar Hugo Herbelin2017-10-10
|/
* [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.
* Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Gravatar Maxime Dénès2017-10-06
|\ | | | | | | "_something")
* \ Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.Gravatar Maxime Dénès2017-10-06
|\ \
* \ \ Merge PR #1069: Improve support for -w optionsGravatar Maxime Dénès2017-10-05
|\ \ \
* \ \ \ Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ | | | | | | | | | | | | | | | to escape non-UTF-8 file names)
* \ \ \ \ Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | coq_makefile are in sync (supersed #1039)…
| | | | * | [pp] Minor optimization in `Pp.t` construction and gluing.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
| | | | * Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | |
| | | | * Distinguishing pseudo-letters out of the set of unicode letters.Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
| | | | * Fixing typos in comments of unicode.ml.Gravatar Hugo Herbelin2017-10-05
| | | | |
* | | | | Merge PR #1100: Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \