Lean Server stopped

Stream: lean4

[Dan Velleman]

In VSCode Lean Infoview, I am getting this message: The Lean Server has stopped processing this file: Server process for file:///... crashed, likely due to a stack overflow or a bug.
Anyone know what's causing this?
My project consists of two files. One file contains a bunch of tactic definitions and examples testing those tactics. That file seems to work just fine. The other file is the Main file, and all it contains is an import command to import the file with the tactic definitions. When I try to view the Main file, I get the error message.

[Chris Lovett]

Can you share a minimal repro and your OS platform details?

[Dan Velleman]

It's a MacBook Pro, MacOS Monterey 12.5.1. (I just update the OS this morning; perhaps that's relevant.)
Lean toolchain is leanprover/lean4:nightly (default)
Lean (version 4.0.0-nightly-2022-08-16, commit 37ba0df5841b, Release)
VSCode is Version 1.70.2.
Not sure what you mean by "minimal repro". The file with the tactic definitions is about 1000 lines. The file that is causing the error is one line--the import command.

[Dan Velleman]

Perhaps I don't understand how packages work. I just tried copying the contents of the large file and saving them in a new file (in the same folder as the other files). Then I changed the import command to import the new file rather than the old one. Now I get the error "unknown package (name of new file)". I assumed that import would simply read in any file I named, but perhaps that's not how it works.
Perhaps my project is configured wrong somehow?

[Chris Lovett]

Yeah, I've been confused about that before also. The way packages work is like this:

lake new Sample

now I have a folder named "Sample" containing a "package" of that name and I can load that folder into VS code and everything is good. Notice "Main.lean" can import the library named "Sample" and that in this case "Sample" is just "Sample.lean" right now - a very simple single file library. The lakefile.lean builds this "Sample" library because of this line:

lean_lib Sample {
  -- add library configuration options here
}

Now if you want to add more files to this library can't just add more files at the top level of your package, instead you have to create a folder named "Sample" and put the files in there. So let's say I do that and add a Hello.lean containing def hello := "friend" then I'll have this structure:

image.png

and the convention then is to change the top level Sample.lean so it contains this: import Sample.Hello and now when you #eval main you will see Hello, friend!. Now Main.lean could also skip Sample.lean and go straight to Hello with this import: import Sample.Hello.

[Dan Velleman]

My package was set up slightly differently--perhaps it was created by an earlier version of lake. I created a new package and copied my tactic definitions into it, and things seem to be working now.
Can I change the setup? I have no use for the Main file--I'm not interested in executing a program, I want to prove theorems, and I want to put my theorems in several files with more meaningful names than "Main". Can I delete Main and create other files for my theorems? If I do, do I have to remove these lines from lakefile.lean:
@[defaultTarget]
lean_exe hTPI {
root := `Main
}
Do I have to have a library file whose name is the same as the name of the package? I'd rather use a different name for my file of tactic definitions. If I put that file inside the appropriate folder, as you did in your example with the the file Hello.lean, can I get rid of the library file at the top level? If so, should I delete these lines from lakefile.lean:
lean_lib HTPI {
-- add library configuration options here
}
Or do those lines also identify the name of the folder where additional library files are to be found? Or is the name of the folder taken from the "package" entry in lakefile.lean?

[Chris Lovett]

Yes, Lean recently moved from lake 3.3 to lake 4.0 and with that came some breaking changes, so rebuilding your lake packages from scratch is probably a good thing to do. So to answer your question, absolutely, Lake can build just a library and no executable program, in fact, lake new Foo lib will do exactly that so you can see what the template is, basically you just remove the lean_exe target and move the @[defaultTarget] to your lean_lib target and you are good to go. And yes, you can also specify multiple lean_lib targets like your HDPI target, and this way you can break up your code into multiple libraries, each in a separate folder. One library can import the other library no problem.

[Chris Lovett]

But if you lookat how mathlib4 is organized, there is only one folder (and only one library) but lots of sub-folders inside that so you can also organize your code that way.

[Dan Velleman]

Thanks Chris. I think I've got my package set up the way I want it now.