leanpkg configure

Stream: lean4

[François G. Dorais]

The current manual says:

There is no integration of leanpkg and the language server at the moment, so the LEAN_PATH, which is the last line returned by leanpkg configure, must be set explicitly before starting the editor. Changes must be saved and compiled with leanpkg build to be visible in other files, which must then be invalidated using an editor command (see links above).

That's interesting... but it's not very detailed. My main issue right now is that import doesn't work as expected, presumably since I never set LEAN_PATH. But leanpkg configure gives me bogus error messages instead of a path:

WARNING: Lean version mismatch: installed version is leanprover/lean4:4.0.0, but package requires leanprover/lean4:4.0.0-m1
configuring lean-2021 0.1
> leanpkg build    # in directory ./src
uncaught exception: no such file or directory (error code: 2)
  file: leanpkg.toml
uncaught exception: external command exited with status 1

The toml file is totally right there. Changing the toml file lean_version to leanprover/lean4:4.0.0 doesn't work either.

I'm moving to a different (better) computer for today but I thought I'd post this in case someone has a similar issue.

[Reid Barton]

I'm getting this error too

[Reid Barton]

It seems to be changing directory to src and then trying to read leanpkg.toml

[Reid Barton]

as a workaround, I'm going to try using path = "." for now

[Sebastian Ullrich]

Ah, I don't think I ever tested path (leanpkg is about a week old...). The tentatively preferred structure in Lean 4 is to put a MyPackage.lean root file right into the repo root (like in e.g. Python), though I don't think we've documented that anywhere aside from the Nix template package...

[Sebastian Ullrich]

If that is in fact how Lean 4 packages will be structured, we should probably remove path

[Sebastian Ullrich]

Note that in Lean 4 there is no default.lean, so having both MyPackage.lean and MyPackage/Foo.lean is no problem.

[François G. Dorais]

@Sebastian Ullrich If path is . then will LEAN_PATH always be ./build?

[Sebastian Ullrich]

Only if you have no dependencies

[Sebastian Ullrich]

I'm working on a solution for both automatically setting up LEAN_PATH and compiling dependencies right from inside the editor though

[François G. Dorais]

I'm still getting Lean version mismatch warnings because lean_version = "leanprover/lean4:4.0.0-m1" is needed for elan to fetch the right lean build but then the installed Lean identifies itself as "leanprover/lean4:4.0.0".

It's just an annoyance, it doesn't seem to affect anything. I can eliminate these warnings using elan override to bypass leanpkg's lean_version.

[Reid Barton]

It took me a while to figure out how to import modules from the same project, so to summarize the information here and elsewhere:

• You must have a single .lean file Foo.lean in the root of your project
• The rest of your files must be in the directory Foo, and import Foo.Bar.Baz will read Foo/Bar/Baz.lean
• You must set LEAN_PATH to the build directory for emacs to tell Lean where to find the modules
• You have to run leanpkg build and M-x lsp-workspace-restart in order to see changes in imported modules

I set LEAN_PATH for my whole tmux session (and also LEAN4=y which I test in my .emacs to know whether to load lean4-mode).

[Scott Kovach]

thanks for documenting this; I discovered these steps myself through trial and error and was about to post something when zulip pointed me to this topic.
if this behavior isn't too tentative it would be helpful to include in the Setup section of the new manual, and maybe leanpkg init could suggestively create the directory Foo in addition to Foo.lean

[Sebastian Ullrich]

I added more documentation and a way to use leanpkg for creating executables in https://github.com/leanprover/lean4/pull/295

[Sebastian Ullrich]

Manually setting LEAN_PATH and running leanpkg build after each change should not be necessary anymore since https://github.com/leanprover/lean4/pull/263