Can I use `buildLeanPackage` with custom lean leanmake lake

Stream: mathlib4

[Alissa Tung]

and leanc?

In the official repo of Lean4 contains a flake, it has an output package buildLeanPackage. I can call buildLeanPackage with custom lean leanmake lake leanc? They comes from I package I had already made

[Joachim Breitner]

The nix setup is not very actively used and maintained, so if you want to go that route, you probably have to answer many questions yourself.

[Alissa Tung]

Joachim Breitner 发言道：

The nix setup is not very actively used and maintained, so if you want to go that route, you probably have to answer many questions yourself.

I will try to write a plain drv to do that, where as the build result in $out will just contains .lake... I am not sure whether this is acceptable for using libraries as dependencies for daily development, and how can I use it though

[Joachim Breitner]

Worth a try. In the long run we probably want a nix setup that builds on top of lake, rather than replicating some of its work; sounds like that is what you have in mind.

[Alissa Tung]

After some inspection on the structure of Nix build outputs, I decide to write a lake2nix package. Wish it goes okay

[Eric Wieser]

Joachim Breitner said:

Worth a try. In the long run we probably want a nix setup that builds on top of lake, rather than replicating some of its work; sounds like that is what you have in mind.

This presumably would need some way to query a dependency graph from lake before building, and a way to ask lake to generate trace files when invoked on a single target?

[Joachim Breitner]

Or forfeit fine-grained derivations, and map lake packages to nix derivations, or even full projects. Kinda sad. It'd not be useful for developing, but for testing , packaging and deployment only, I fear

[Joachim Breitner]

Alissa Tung said:

After some inspection on the structure of Nix build outputs, I decide to write a lake2nix package. Wish it goes okay

Prior (and AFAIK) discontinued work at https://github.com/Kha/nale