Topic: leanpkg configure
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.
Reid Barton (Jan 08 2021 at 00:11):
I'm getting this error too
Reid Barton (Jan 08 2021 at 00:14):
It seems to be changing directory to
src and then trying to read
Reid Barton (Jan 08 2021 at 00:14):
as a workaround, I'm going to try using
path = "." for now
Sebastian Ullrich (Jan 08 2021 at 10:17):
Ah, I don't think I ever tested
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 (Jan 08 2021 at 10:18):
If that is in fact how Lean 4 packages will be structured, we should probably remove
Sebastian Ullrich (Jan 08 2021 at 10:20):
Note that in Lean 4 there is no
default.lean, so having both
MyPackage/Foo.lean is no problem.
François G. Dorais (Jan 08 2021 at 10:26):
@Sebastian Ullrich If path is
. then will LEAN_PATH always be
Sebastian Ullrich (Jan 08 2021 at 10:27):
Only if you have no dependencies
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
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.
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
Foo.leanin the root of your project
- The rest of your files must be in the directory
import Foo.Bar.Bazwill read
- You must set
builddirectory for emacs to tell Lean where to find the modules
- You have to run
M-x lsp-workspace-restartin order to see changes in imported modules
LEAN_PATH for my whole tmux session (and also
LEAN4=y which I test in my
.emacs to know whether to load
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
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
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