Zulip Chat Archive

Stream: lean4

Topic: leanpkg configure


view this post on Zulip François G. Dorais (Jan 05 2021 at 15:20):

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.

view this post on Zulip Reid Barton (Jan 08 2021 at 00:11):

I'm getting this error too

view this post on Zulip Reid Barton (Jan 08 2021 at 00:14):

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

view this post on Zulip Reid Barton (Jan 08 2021 at 00:14):

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

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 10:17):

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

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 10:18):

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

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 10:20):

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

view this post on Zulip François G. Dorais (Jan 08 2021 at 10:26):

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

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 10:27):

Only if you have no dependencies

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 10:29):

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

view this post on Zulip François G. Dorais (Jan 08 2021 at 10:34):

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.

view this post on Zulip Reid Barton (Jan 08 2021 at 14:46):

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

view this post on Zulip Scott Kovach (Jan 20 2021 at 20:09):

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

view this post on Zulip Sebastian Ullrich (Jan 25 2021 at 15:51):

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

view this post on Zulip Sebastian Ullrich (Jan 25 2021 at 15:52):

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


Last updated: May 07 2021 at 12:15 UTC