lake package root case-sensitivity

Stream: general

[Enrico Borba]

How does lake know the root of a lean package? For example, in mathlib's lakefile.lean specifies the package name as mathlib, (note the lower case), and yet lake when building knows that the root is Mathlib.lean. Does lake look for case <package-name>.lean with case-insensitivity?

[Enrico Borba]

Nvm, from lake's readme:

It will also create the root Lean file for the package's library, which uses the capitalized version of the package's name (e.g., Hello.lean in this example), and the root file for the package's binary Main.lean. They contain the following dummy "Hello World" program split across the two files:

[Mario Carneiro]

The library is called Mathlib

[Mario Carneiro]

the package name is pretty much unused except for lake internal stuff: it is the name used in require lines, and the name of the directory in lake-packages for a dependency, but the modules themselves are named based on the library name or the roots/globs of the library

[Enrico Borba]

Oh the fact that it's used in lake-packages is good to know.

[Enrico Borba]

I'm writing a best-effort lake2nix and was /hoping/ not to have to parse/run any lakefile.lean. The one I have now works and can compile mathlib OK, but I have to manually inject the library name for ProofWidgets, since it's referred to in the manifest as proofwidgets but the library name is in fact ProofWidgets.

[Enrico Borba]

ah I see now the lean_lib statements in the lakefile.lean.

[Enrico Borba]

I have a small question though, mathlib's lakefile.lean defines a few libs. When mathlib is declared as a dependency in lake-manifest.json, are all of those lean_lib libraries available?

[Scott Morrison]

Yes.

[Mario Carneiro]

Enrico Borba said:

I'm writing a best-effort lake2nix and was /hoping/ not to have to parse/run any lakefile.lean. The one I have now works and can compile mathlib OK, but I have to manually inject the library name for ProofWidgets, since it's referred to in the manifest as proofwidgets but the library name is in fact ProofWidgets.

Don't do it, this is not a supported configuration. You should petition @Mac Malone to make this more possible in the future

[Mario Carneiro]

The workaround solution until then is to use something like https://github.com/digama0/lean-cache/tree/main/lake-ext , which is the out-of-tree version of lake dump-config which has an uncertain future

[Mauricio Collares]

Not sure if https://github.com/Kha/nale/tree/master/lake2nix is still up-to-date

[Mario Carneiro]

lol, LakeExport.lean is almost exactly the same thing as lake-ext

[Mario Carneiro]

unfortunately it doesn't have a lean-toolchain so I'm not sure how old it is, but from the modification dates I would guess lake-ext is newer

[Mauricio Collares]

It does have a flake.lock pinned at http://github.com/leanprover/lean4/commit/1a6663a41baf95cb995b79cd8a466ab81e230b35 though

[Eric Wieser]

Is there any way to get these nix builds to generate the trace/hash files you need to actually open a project in vscode? Otherwise lake just rebuilds everything anyway, right?

[Mauricio Collares]

That's a question I'd like to know the answer to as well. One use case that doesn't require this is shipping a program written in Lean. Admittedly this would make more sense with Std instead of Mathlib, in which case there would be no dependency problems, but it's not too far-fetched to have something which produces a binary and depends on Mathlib

[Eric Wieser]

I mean I guess you can always make a custom binary that just pokes at lake implementation details to write a hash, but that's obviously rather fragile

[Joachim Breitner]

I (personal me, not FRO me) am using nix to build and deploy loogle, which does include Mathlib as a dependency. But the way I'm doing that is a bit hackish and wouldn’t scale to public consumption. So I’d be grateful for a good …2nix setup for building lean programs, while I personally don’t need it for development. It’s probably tricky, though.

[Enrico Borba]

Mario Carneiro said:

Enrico Borba said:

I'm writing a best-effort lake2nix and was /hoping/ not to have to parse/run any lakefile.lean. The one I have now works and can compile mathlib OK, but I have to manually inject the library name for ProofWidgets, since it's referred to in the manifest as proofwidgets but the library name is in fact ProofWidgets.

Don't do it, this is not a supported configuration. You should petition Mac Malone to make this more possible in the future

I definitely don't have any expectations of support, it's just what I use for my personal configuration.

[Enrico Borba]

Joachim Breitner said:

I (personal me, not FRO me) am using nix to build and deploy loogle, which does include Mathlib as a dependency. But the way I'm doing that is a bit hackish and wouldn’t scale to public consumption. So I’d be grateful for a good …2nix setup for building lean programs, while I personally don’t need it for development. It’s probably tricky, though.

My approach was actually inspired by the loogle one. I just didn't like having to manually specify the commits, so I walk the refs in lake-manifest.json in order to automate fetching the dependencies.

[Enrico Borba]

Eric Wieser said:

Is there any way to get these nix builds to generate the trace/hash files you need to actually open a project in vscode? Otherwise lake just rebuilds everything anyway, right?

Sorry for the noob question (just looking to understand lean packaging/distribution a bit more): What do you mean by "trace/hash" files that you "need to actually open a project"? Does this have to do with setting LEAN_PATH? Or something else

[Eric Wieser]

I mean the files that end up in build/lib/MyFile.olean.hash and build/lib/MyFile.trace

[Eric Wieser]

My attempt was:

import Lake.Build.Common
import Lake.Load.Main
import Lake.CLI.Main

open Lake

#eval Lake.CliM.run (do
  processOptions lakeOption
  let config ← mkLoadConfig (← getThe LakeOptions)
  let ws := ←Lake.loadWorkspace config
  dbg_trace config.configFile
  let b := Lake.fetchFileTrace (System.mkFilePath ["Std.lean"])
  let t := ← ws.runBuild b
  dbg_trace t.hash
  return
  ) []

but this crashes the web editor