aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-10Add minimal CHANGES entry about compat notationsJason Gross
2018-10-10Merge PR #8384: Small fixes in attribute documentation.Clément Pit-Claudel
2018-10-10Merge 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-10Merge PR #8693: [test-suite] rename a filePierre-Marie Pédrot
2018-10-10[test-suite] rename a fileVincent Laporte
2018-10-10Merge PR #8651: [dune] Provide an optimized build profile with inlining reports.Pierre-Marie Pédrot
2018-10-10Merge PR #6218: Fix #5197, handling of algebraic universesPierre-Marie Pédrot
2018-10-10Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit ↵Enrico Tassi
tests.
2018-10-10Merge PR #8679: [test suite] Compile test cases, instead of only loading themEnrico Tassi
2018-10-10Merge PR #8457: Refactoring of Micromega plugin (including new Simplex based ↵Vincent Laporte
solver)
2018-10-09Merge 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-suiteVincent Laporte
2018-10-09[test-suite] use “-async-proofs-cache force” when compilingVincent Laporte
2018-10-09[default.nix] some fixesVincent 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 casesVincent Laporte
2018-10-09[test-suite] ensure file names are valid module namesVincent Laporte
2018-10-09Refactoring of Micromega code using a Simplex linear solverFré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-09Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build.Pierre-Marie Pédrot
2018-10-08Merge PR #8676: Fixes #8672: ill-formed pattern substitution in notation ↵Emilio Jesus Gallego Arias
with "let"
2018-10-08Merge PR #8674: [ci] Add aac-tactics.Emilio Jesus Gallego Arias
2018-10-08Fixes #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-08Merge PR #8677: [dune] Fix bad interaction among PR #8627 and #8657Maxime Dénès
2018-10-08[dune] Fix bad interaction among PR #8627 and #8657Emilio 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-08Merge PR #8657: [dune] Refactor files following advice from upstream.Théo Zimmermann
2018-10-08Merge PR #8654: Remove FCast from CClosure.fterm.Maxime Dénès
2018-10-08Fix #5197, handling of algebraic universesMatthieu 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-08Remove 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-08Merge PR #8660: Issue 8659 not always build all addonsThéo Zimmermann
2018-10-08Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune.Théo Zimmermann
2018-10-08Merge PR #8585: Simplify declaration of universe namesPierre-Marie Pédrot
2018-10-08Merge PR #8668: Missing headers in two filesThéo Zimmermann
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-08Merge PR #8582: [api] Deprecate `evar_map` ref combinators.Pierre-Marie Pédrot
2018-10-07Adding missing header in functional_principles_types.ml.Hugo Herbelin
2018-10-07Adding 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-07Merge PR #8493: [api] Remove (most) 8.9 deprecated objects.Pierre-Marie Pédrot
2018-10-06Merge 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-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05Merge 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-05Merge PR #8658: Remove duplicate committers.Théo Zimmermann
2018-10-05Merge 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:04:51 +0000