| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-10 | [dune] Require that `plugin_base.dune` exists in plugin dirs. | Emilio Jesus Gallego Arias | |
| `coq_dune` should not consider a directory as a plugin one if the `plugin_base.dune` file doesn't exists, as the generated `dune` file for that dir will try to include it. We have had problems with this in the past due to spurious dirs. | |||
| 2018-10-10 | Merge PR #8692: [test-suite] Don't reset `OCAMLPATH`, but append to it. | Enrico Tassi | |
| 2018-10-10 | [test-suite] Don't reset `OCAMLPATH`, but append to it. | Emilio Jesus Gallego Arias | |
| This fixes an obvious bug introduced in #8602. | |||
| 2018-10-10 | Merge PR #8693: [test-suite] rename a file | Pierre-Marie Pédrot | |
| 2018-10-10 | [test-suite] rename a file | Vincent Laporte | |
| 2018-10-10 | Merge PR #8651: [dune] Provide an optimized build profile with inlining reports. | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #6218: Fix #5197, handling of algebraic universes | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit ↵ | Enrico Tassi | |
| tests. | |||
| 2018-10-10 | Merge PR #8679: [test suite] Compile test cases, instead of only loading them | Enrico Tassi | |
| 2018-10-10 | Merge PR #8457: Refactoring of Micromega plugin (including new Simplex based ↵ | Vincent Laporte | |
| solver) | |||
| 2018-10-09 | Merge PR #8673: Remove dead code in universe handling in the abstract tactical. | Gaëtan Gilbert | |
| 2018-10-09 | [dune] Provide an optimized build profile with inlining reports. | Emilio Jesus Gallego Arias | |
| This satisfies a wish by @ppedrot | |||
| 2018-10-09 | [default.nix] Add install dir to OCAMLPATH before running the test-suite | Vincent Laporte | |
| 2018-10-09 | [test-suite] use “-async-proofs-cache force” when compiling | Vincent Laporte | |
| 2018-10-09 | [default.nix] some fixes | Vincent Laporte | |
| 2018-10-09 | [test-suite] Use ocamlfind to locate Coq libraries in unit tests. | Emilio Jesus Gallego Arias | |
| This is slightly more robust and allows to run the test suite with Dune which may place OCaml objects differently. | |||
| 2018-10-09 | [test-suite] compile (rather than load) test cases | Vincent Laporte | |
| 2018-10-09 | [test-suite] ensure file names are valid module names | Vincent Laporte | |
| 2018-10-09 | Refactoring of Micromega code using a Simplex linear solver | Frédéric Besson | |
| - Simplex based linear prover Unset Simplex to get Fourier elimination For lia and nia, do not enumerate but generate cutting planes. - Better non-linear support Factorisation of the non-linear pre-processing Careful handling of equation x=e, x is only eliminated if x is used linearly - More opaque interfaces (Linear solvers Simplex and Mfourier are independent) - Set Dump Arith "file" so that lia,nia calls generate Coq goals in filexxx.v. Used to collect benchmarks and regressions. - Rationalise the test-suite example.v only tests psatz Z example_nia.v only tests lia, nia In both files, the tests are in essence the same. In particular, if a test is solved by psatz but not by nia, we finish the goal by an explicit Abort. There are additional tests in example_nia.v which require specific integer reasoning out of scope of psatz. | |||
| 2018-10-09 | Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build. | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8676: Fixes #8672: ill-formed pattern substitution in notation ↵ | Emilio Jesus Gallego Arias | |
| with "let" | |||
| 2018-10-08 | Merge PR #8674: [ci] Add aac-tactics. | Emilio Jesus Gallego Arias | |
| 2018-10-08 | Fixes #8672 (ill-formed pattern substitution in notation with "let"). | Hugo Herbelin | |
| 2018-10-08 | [ide] [dune] [test-suite] Reorganize `fake_ide` build. | Emilio Jesus Gallego Arias | |
| Even if `fake_ide` was under tools, it depended on libraries from `ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the test-suite [this means `test-suite` depends on the `ide` folder then]. In the Dune side, we reorganize libraries so `fake_ide` doesn't depend on GTK anymore, this allows to run the test-suite when GTK is not available. In order to achieve this, we had to split the `coqide` package in a server and client version. | |||
| 2018-10-08 | [ci] Add aac-tactics. | Théo Zimmermann | |
| And fix a typo that was previously there. | |||
| 2018-10-08 | Merge PR #8677: [dune] Fix bad interaction among PR #8627 and #8657 | Maxime Dénès | |
| 2018-10-08 | [dune] Fix bad interaction among PR #8627 and #8657 | Emilio Jesus Gallego Arias | |
| Dangers of not stacking PRs hit again, and here we hit a problem breaking the build on master due to #8627 adding a new file to install with for the (implicit) `coq` package and #8657 removing the implicit status of such package. | |||
| 2018-10-08 | Merge PR #8657: [dune] Refactor files following advice from upstream. | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8654: Remove FCast from CClosure.fterm. | Maxime Dénès | |
| 2018-10-08 | Fix #5197, handling of algebraic universes | Matthieu Sozeau | |
| They were allowed to stay in terms in some cases. We now ensure that if an evar is defined as e.g. fun x => Type@{foo}, foo is properly refreshed to be non-algebraic as it could otherwise appear in the term and break the invariant. Also cleanup the implementation of refresh_universes to avoid using a mutable reference and simply rely on the Constr.map smartmap idiom instead. This might have compatibility issues, e.g. in HoTT where maybe more non-algebraic proxy universes could be generated, we'll see. For the bug report proper, there is a lack of bidirectional type-checking that makes the initial definition fail (there's a non-canonical choice of dependency if we don't consider the typing constraint). With the Program bidir hint it passes. | |||
| 2018-10-08 | Remove dead code in universe handling in the abstract tactical. | Pierre-Marie Pédrot | |
| Since 213b323 the kernel was expecting to receive an empty set of internal universe constraints in polymorphic definitions. We lift this invariant to the code that actually generates side effects. | |||
| 2018-10-08 | Merge PR #8660: Issue 8659 not always build all addons | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune. | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8585: Simplify declaration of universe names | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8668: Missing headers in two files | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8630: Some cleaning in the test suite | Enrico Tassi | |
| 2018-10-08 | Merge PR #8554: Fixes #8553: regression of tactic "change" under binders. | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8582: [api] Deprecate `evar_map` ref combinators. | Pierre-Marie Pédrot | |
| 2018-10-07 | Adding missing header in functional_principles_types.ml. | Hugo Herbelin | |
| 2018-10-07 | Adding missing header to comFixpoint.ml. | Hugo Herbelin | |
| 2018-10-07 | [api] Deprecate `evar_map` ref combinators. | Emilio Jesus Gallego Arias | |
| All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the combinators to discourage this style of programming. Still a few places do use imperative style, but they are pretty localized and should be cleaned up separately. As these are the last bits of `e_` API remaining this PR closes #6342. | |||
| 2018-10-07 | Merge PR #8493: [api] Remove (most) 8.9 deprecated objects. | Pierre-Marie Pédrot | |
| 2018-10-06 | Merge PR #7850: Rewrite CEphemeron to use a type-safe implementation based ↵ | Pierre-Marie Pédrot | |
| on GADTs | |||
| 2018-10-06 | [api] Remove (most) 8.9 deprecated objects. | Emilio Jesus Gallego Arias | |
| A few of them will be of help for future cleanups. We have spared the stuff in `Names` due to bad organization of this module following the split from `Term`, which really difficult things removing the constructors. | |||
| 2018-10-06 | Merge PR #8555: Remove section paths from kernel names | Pierre-Marie Pédrot | |
| 2018-10-05 | Merge PR #8662: Fix printing of raw terms for lambda's without parameters ↵ | Emilio Jesus Gallego Arias | |
| (continued, adding smart constr_expr binder constructors) | |||
| 2018-10-05 | Merge PR #8658: Remove duplicate committers. | Théo Zimmermann | |
| 2018-10-05 | Merge PR #8645: Improve markdown in changes. | Théo Zimmermann | |
| 2018-10-05 | [dune] Refactor files following advice from upstream. | Emilio Jesus Gallego Arias | |
| After some discussion upstream, I think that for the current a multi-package setup in a single repository this setup saves a bit work. The most problematic bit is the `-rectypes` flag; its status is not saved per-library so we must either duplicate the flags in the coqide scope (scope == dune-project file), or unify its scope with Coq. We do this last option as this seems like the easiest thing for now. Changes: - Move coqide.opam file to the root, use a single scope/`dune-project` file. - Remove `dune-workspace`, this should be owned by the developer / user. | |||
| 2018-10-05 | Merge PR #8661: CI: fix Iris and stdpp ref selection | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |