lake

lake copied to clipboard

Incorrect/unhelpful "error parsing lakefile" from `print-paths`

8

In a file I get ``` `/home/sebastian/.elan/toolchains/leanprover--lean4---nightly-2022-08-10/bin/lake print-paths Init` failed: stderr: Error parsing '././lakefile.lean'. Please restart the lean server after fixing the Lake configuration file. ``` but going back to...

Kha

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...

gebner

`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...

gebner

Support building dynamic libraries by default

4

I'm having trouble setting up a build for dynamic libraries. I can still do `lake build Foo:shared` but I'm unable to successfully set up the lakefile such that `lake build...

lecopivo

Currently Lake seems to reject a statement such as ```lean target myTarget (pkg : Package) (arg : Nat) : FilePath := ... ``` We can write ```lean def myTarget (pkg...

Vtec234

Support different "environments" / non-mandatory dependencies

8

(I'm assuming this has at least been thought about, but filing it since I don't see another place tracking it). I'd like to add a dev dependency which isn't/shouldn't be...

Julian

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...

gebner

Lake serve has become 50% slower since 3.2.1

2

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

gebner

As discussed previously in the Zulip it would be beneficial if Lake could output a graph representation of the dependencies it has discovered. In order to replace the Lake dependency...

hargoniX

I'm not completely sure what the right API would be. It would be nice to be able to have something like `inputFileTarget` but to specify a directory for whole directories....

EdAyers