aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | * | | | | | | | | | | Fix TypeclassDebug.out after conflicting PR mergesGravatar Matthieu Sozeau2017-07-26
| |_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | test-suite/success/extraction.v : add some Extraction TestCompileGravatar Pierre Letouzey2017-07-26
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | Enrich test file 4720.v with a compilation test of the extracted codeGravatar Pierre Letouzey2017-07-26
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |
| | | | | | | | | | * | | | | adding a test-suite file 4709.v (thanks to the new command Extraction ↵Gravatar Pierre Letouzey2017-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | TestCompile)
| | | | | | | | | | * | | | | Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Pierre Letouzey2017-07-26
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | |
| | | | | | | | | | | | * | Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |
| | | | | | | | | | * | | Add a comment regarding the specialization of the combinator in Detyping.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4844 and 4824)
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #910: Add [opam update] and online repository to gitlab CI script.Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | | Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | |/ / / / | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes bug 5650: evar (x : Prop) should not be slow.
* | | | | | | | | | | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions fileGravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #902: Only perform profile initialization and printing when the ↵Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | flag is set.
| | | | | | | | | * | | | | | | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | |/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* | | | | | | | | | | | | | | Merge PR #894: Fixing a little location bug with recursive bindersGravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #882: Adding a V8.7 compatibility version number.Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | | | | Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ought to ease the understanding of the code.
| | | | | | | | | | * | | | | | | 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 #885: Removing a dummy parameter in some FMapPositive statements.Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * | | | Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
* | | | | | | | | | | | | | | | Merge PR #868: Fix debug trace of typeclasses eauto.Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #845: Add Z.mod_div lemma to standard library.Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | | | | | | | | | * | Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs ↵Gravatar Pierre Letouzey2017-07-25
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4844 and 4824) The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic (otherwise type parameters would have to be propagated out of any type definition involving Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any, as shown by the examples in bug reports 4844 and 4824. This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations. We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _]. NB: even if the original bug report mentions universe polymorphism, this issue is almost unrelated to it. It just happens that when universe polymorphism is off, an inductive instance is fully placed in Prop (cf. template polymorphism) in the example, avoiding triggering the issue. Warning: the test-suite file is there for archiving the repro case, but currently it doesn't test much (we should run ghc on the extracted code).
| | | | | | | * | | | | | | | | | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)Gravatar Maxime Dénès2017-07-21
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | * | No useless reallocation in Termops.collapse_appl.Gravatar Pierre-Marie Pédrot2017-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This function is suspicious, and reallocates a lot when it should be the identity. This matters for detyping, where it is about the only place where it is used.
| | | | | | | | | | | | | | | | * | Allocation-friendly detyping of term arrays.Gravatar Pierre-Marie Pédrot2017-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is important for externalization big terms. We were indeed allocating twice as much as needed lists for the application node case, as the Array.map_to_list function is exactly List.map o Array.to_list. We could probably tweak this function instead, at the expense that order of evaluation is not guaranteed. I'm not willing to do that though.
| * | | | | | | | | | | | | | | | | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Gravatar Maxime Dénès2017-07-21
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | * | | | | | | Add [opam update] and online repository to gitlab CI script.Gravatar Gaëtan Gilbert2017-07-21
| | | | | | | | | | | | |_|_|_|/ / | | | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows it to find out about new packages / compilers without having to invalidate cache somehow. Additionally the latest camlp5 (7.01) is not in the local repository for some reason.
| | | | | | | | | | | | | | | * | Alternate way of doing timing on ciGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This puts the boilerplate all in one place
| | | | | | | | | | | | | | | * | Separate make from python script for HoTTGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
| | | | | | | | | | | | | | | * | Display timing data travis for various projectsGravatar Jason Gross2017-07-21
| | | | | | | | | | | | |_|_|/ / | | | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | HoTT, which builds it's own makefile, and supports timing data, makes use of its own timing script. Everything else goes through the coq-bundled timing scripts.
| * | | | | | | | | | | | | | | 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
| | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:37:01 +0000