| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Note that since this now reduces before restricting universes
behaviour may be a bit different.
|
|
See commit [Simplify code for [Definition := Eval ...]] which without
this breaks test suite 7631.v
|
|
|
|
|
|
|
|
|
|
- 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.
|
|
|
|
with "let"
|
|
|
|
|
|
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.
|
|
And fix a typo that was previously there.
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
on GADTs
|
|
|
|
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.
|
|
|
|
(continued, adding smart constr_expr binder constructors)
|
|
Issue #8533 is still unmitigated.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
This was broken due to a typo when introducing the archive download
method.
We also remove default [master] values from basic-overlay which hid
this issue.
|
|
|
|
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
