Gabriel Ebner

When displaying sequents of formulas with different height, the formula will currently be aligned based on the (vertical) center of their image rendering: ``` scala prooftool(solveQuasiPropositional(hof"a != b b !=...

The original CERES takes a proof in LK with quantified cuts, and produces a proof in LK with only atomic cuts. This is done by reducing the problem of cut-elimination...

At the last DK retreat, Martina Seidl (I think) suggested a QBF solver interface for GAPT. This would be a nice, non-critical project for someone who wants to get started...

``` scala prooftool(Escargot getExpansionProof hof"!x?y x=y") ``` Try to click on `∃y`. The only way to expand the `∃y` quantifier is to first click twice on the universal quantifier, it...

When exporting problems to TPTP, not all names can be exported as is, for example `β` is not a valid TPTP identifier, no matter how you encode it. ``` scala>...

The MaxSAT interface allows you to pass arbitrary formulas weights as soft "clauses". It can happen that the CNF of such a soft formula does not have exactly one clause....

fix: also update when inputRev changes

3

It turns out that #119 already worked in some cases. Namely `lake update` would pick up changes in transitive dependencies, but only if the `inputRev` stayed the same. If the...

`lake update` does not pick up updates from transitive dependencies

3

For example `mathlib3port` depends on `lean3port` which depends on `mathlib4`. But running `lake update` in `mathlib3port` does not pick up the new `mathlib4` version when `lean3port` updates its dependency. We...

Declare extra dependencies of Lean files

13

Lean files can use elaborators that read files at compile time. For example `include_str` in doc-gen4 reads the specified file during compilation and inserts the file's contents as a string...

Lake serve has become 50% slower since 3.2.1

2

``` cd lake git checkout v3.2.1 time lake serve