aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | This was an easy to prove property that I somehow overlooked.
* Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | This is actually useless, the code does not depend on the value of the entry for side-effects.
* Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment.
* More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants.
* Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
|
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
* Merge PR #905: [api] Remove type equalities from API.Gravatar Maxime Dénès2017-07-26
|\
* \ Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \
* \ \ Merge PR #859: Extraction TestCompileGravatar Maxime Dénès2017-07-26
|\ \ \
* \ \ \ Merge PR #808: [api] Put some order in API.mliGravatar Maxime Dénès2017-07-26
|\ \ \ \
* \ \ \ \ Merge PR #750: Remove deprecated options of ./configure in 8.8Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \
| | | | | * make sure that API-leaks cannot be reintroduced by mistakeGravatar Matej Košík2017-07-26
| | | | | |
* | | | | | Makefile.ide: restore a coqide-binaries rule (fix bug 5667)Gravatar Pierre Letouzey2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | This rule is used by opam package coq-coqide
| | | | | * [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | |_|/ | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
| | * | | [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations.
* | | | Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)Gravatar Maxime Dénès2017-07-21
|\ \ \ \
| * | | | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Gravatar Maxime Dénès2017-07-21
| | | | |
| * | | | Install time command under Cygwin (required for timing scripts).Gravatar Maxime Dénès2017-07-21
| | | | |
| | | | * Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Avoid Anomaly (or Assert False) when a module signature contains an applied functor followed by a "with Definition" or "with Module" Also fix the dependency computation in presence of a "with Definition" Concerning 4720, the code extracted out of this bug report was suboptimal in Coq 8.4 (it was compilable, but could have probably been tweaked into a real issue producing faulty code). But the example of 4720 (and some variants of it) was broken since 8.5, for the same reasons as 5177 and 5240. And the good news is that after these repairs, the example of bug 4720 is now extracted to correct code (the "with" is preserved).
* | | | | Merge PR #892: Improve do_split option of typeclass resolutionGravatar Maxime Dénès2017-07-20
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | * | | fake_ide: do as coqide to find out coqtop pathGravatar Enrico Tassi2017-07-20
| | | | |
| | * | | coq_makefile: use System.exists_dir for better portabilityGravatar Enrico Tassi2017-07-20
| | | | |
| | * | | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)Gravatar Enrico Tassi2017-07-20
| | | | |
| | * | | coq-makefile: strip windows drive letter when DESTDIR is not emptyGravatar Enrico Tassi2017-07-20
| | | | | | | | | | | | | | | | | | | | | | | | | In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows.
| | * | | coq-makefile: treat coq_makefile as any other coq binaryGravatar Enrico Tassi2017-07-20
| | | | | | | | | | | | | | | | | | | | In particular, find it under $(COQBIN)
| | * | | more verbose logs for coq-makefileGravatar Enrico Tassi2017-07-20
| | | | |
| | * | | coq-makefile: quote using ' to preserve \ (windows paths)Gravatar Enrico Tassi2017-07-20
| | | | |
| | * | | coq-makefile: make test suite detect more errorsGravatar Enrico Tassi2017-07-20
| | | | | | | | | | | | | | | | | | | | Replacing ; with && and enabling bash's pipefail option
| | * | | In fake_ide, call coqtop.exe instead of coqtop on Win32.Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Avoid using unsupported signals under Windows in fake_ide.Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Remove trailing CR before diff in output and misc tests.Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Print failure logs on appveyor.Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Remove non-terminating Timeout tests from Hints.v.Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Make coqlib relative in test suite (revert 024a7ab20b0)Gravatar Maxime Dénès2017-07-20
| | | | |
| | * | | Add AppVeyor infrastructure, launching the test suite under Windows.Gravatar Maxime Dénès2017-07-20
| |/ / / |/| | |
* | | | Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal.Gravatar Maxime Dénès2017-07-20
|\ \ \ \
* \ \ \ \ Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR #903: Documenting the purity / marshallability invariant of ↵Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | persistent states.
| * | | | | | Documenting the purity / marshallability invariant of persistent states.Gravatar Pierre-Marie Pédrot2017-07-20
| | | | | | |
* | | | | | | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: CheckerGravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #877: Travis+4.05.0Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge PR #745: Add timing scriptsGravatar Maxime Dénès2017-07-19
| |\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ Merge PR #855: Deprecate options that were introduced for compatibility with ↵Gravatar Maxime Dénès2017-07-19
| |\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8.5.
* | \ \ \ \ \ \ \ \ \ \ \ Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | [proofs] Remove circular dependency from Proofview to Goal.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.
* | | | | | | | | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Maxime Dénès2017-07-19
|\ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 06:05:38 +0000