lean server launch directory

[williamstein]

REQUESTED BY>: Patrick Massot

'The only thing that seems to be slightly annoying is that the Lean server seems to be always launched from the home directory. So the leanpkg.path file, which tells lean where are imported files, should be in the project home directory. In VScode we have "Open folder" from the file menu which makes the Lean extension to launch the lean server from the folder.'

I guess we would change things so when you create a foo.lean file in some directory bar, the lean server is launched in the directory bar. It seems like this should be a small somewhere around here:

https://github.com/sagemathinc/cocalc/blob/master/src/smc-project/lean/lean.ts#L68

[williamstein]

I guess we would change things so when you create a foo.lean file in some directory bar, the lean server is launched in the directory bar.

Or maybe that would be totally wrong? Maybe it needs to scan bar and directories above for some special file? What's the best heuristic? Or should it be configurable somehow in some panel? I don't know exactly what to even implement here.

[PatrickMassot]

I think the correct thing to do is to look for leanpkg.path in any directory above the current file, and start Lean from the directory containing leanpkg.path. If this is nowhere, then look for $HOME/.lean/ and start lean from there if it exists. Otherwise start as you do it now (the user will then deserve any inconvenience that may arise).

Maybe @gebner or @Kha can give a more authoritative answer.

[gebner]

I think the correct thing to do is to look for leanpkg.path in any directory above the current file, and start Lean from the directory containing leanpkg.path. If this is nowhere, then look for $HOME/.lean/ and start lean from there if it exists.

This is exactly what happens. (Under the hood, the emacs mode parses the output of lean -p and uses the directory of the leanpkg_path_file field. But it amounts to the same thing.)

[haraldschilly]

I see, i.e. running (or an equivalent of) lean -p | jq '.leanpkg_path_file' | xargs dirname does the trick. Here is a brief session (empty directory):

~/scratch/proj1$ ls
~/scratch/proj1$ lean -p | jq '.leanpkg_path_file' | xargs dirname 
/home/user/.lean
~/scratch/proj1$ touch leanpkg.path
~/scratch/proj1$ lean -p | jq '.leanpkg_path_file' | xargs dirname 
/home/user/scratch/proj1
~/scratch/proj1$ mkdir foo
~/scratch/proj1$ cd foo/
~/scratch/proj1/foo$ touch bar.lean
~/scratch/proj1/foo$ lean -p | jq '.leanpkg_path_file' | xargs dirname 
/home/user/scratch/proj1

[semorrison]

I just ran into this today, and discovered the "put everything in the home directory" workaround. Thanks @PatrickMassot for pointing me here. Besides this, Lean is working really beautifully in cocalc (and I just subscribed for a 4 month course!)

[haraldschilly]

Here is a revised logic, which I think is what we should do.

1. run lean -p in the directory of the .lean file in the editor. it returns json, parse it.
2. field is_user_leanpkg_path is either true | false
   2.1 if true start the server in $HOME, i.e. it will then use the info in~/.lean/...
   2.2 if false start the server in directory of the path in the field leanpkg_path_file. e.g. when I'm in ~/lean-test/foo/ and the path file is in ~/lean-test, this is /home/user/lean-test/leanpkg.path and the server should start in /home/user/lean-test/

[williamstein]

Right now there is one lean server for all lean files, so a major architectural change would be needed too...