Lean4 projects in varied subdirectories in a container

Stream: new members

[Kevin Sullivan]

We want to (1) have Lean4 projects, as created using lake new, in subdirectories scattered across a larger codebase, and (2) use VSCode with remote containers as an IDE. It doesn't work. The problem is that imports are broken, not for lean but for lean4-vscode. If I use "lake new" to create a new Lean project somewhere in the directory structure of a larger project the imports fail. Lake build works, but the VSCode extension doesn't. To see for yourself, use lake new to create a project somewhere other than at the top level project directory. Then open the generated Main.lean code. VSCode will report that the package isn't known. I'm a bit pessimistic about short-term, easy fixes, but am hoping for an upside surprise.

[Kevin Sullivan]

To clarify one thing. The "lake build" command builds a binary, so for the "compiler," the imports are working. But the Lean4 VSCode plugin (or language server?) states that the module name is unknown, with a red squiggly underline with a tooltip to communicate the point. The Lean server then gives up, as reported by VSCode, making VSCode editing of Lean components not so useful (?) in this kind of case.

[Damiano Testa]

I am not sure that I follow what the issue is, but it looks like this thread may be relevant?

[Kevin Sullivan]

Damiano Testa said:

I am not sure that I follow what the issue is, but it looks like this thread may be relevant?

Thank you. The work reported there appears to allow different toolchains to be used for different, and for nested, packages. It's close, but doesn't address the problem of the broken importing function in lean4-vscode.

[Marc Huisinga]

When you mention creating a project inside of the "top level project directory", are both of those projects Lean projects? (I.e. do they both contain a lean-toolchain file)?

[Kevin Sullivan]

Marc Huisinga said:

When you mention creating a project inside of the "top level project directory", are both of those projects Lean projects? (I.e. do they both contain a lean-toolchain file)?

Here are simple instructions to reproduce.

Somewhere on your file system do this:

mkdir foo
cd foo
mkdir bar
cd bar
lake init
cd ..
code .

Now open bar/Main.lean

[Marc Huisinga]

This works perfectly fine on my end. What's your Lean 4 VS Code extension version?

[Kevin Sullivan]

Marc Huisinga said:

This works perfectly fine on my end. What's your Lean 4 VS Code extension version?

v0.0.95
lean4-vscode_screen.jpg

[Marc Huisinga]

Kevin Sullivan said:

Marc Huisinga said:

This works perfectly fine on my end. What's your Lean 4 VS Code extension version?

v0.0.95

The current version is v0.0.160. How did you even get stuck with such an old version? 0.0.95 is from Aug 30, 2022.

[Kevin Sullivan]

Marc Huisinga said:

Kevin Sullivan said:

Marc Huisinga said:

This works perfectly fine on my end. What's your Lean 4 VS Code extension version?

v0.0.95

The current version is v0.0.160. How did you even get stuck with such an old version? 0.0.95 is from Aug 30, 2022.

Yikes, it's what's in the extensions repo, as far as I can tell! Screen grab attached.

vscode2.jpg

[Marc Huisinga]

OK, looking at what happened in 0.0.96, I might have an idea for why you are stuck on such an old version: Your VS Code is probably severely outdated. In 0.0.96 the minimum VS Code version requirement of the extension was bumped to 1.70.0 from 1.61.0. Your VS Code version is probably somewhere between those and VS Code will not update extensions anymore if it does not fulfill the version requirement.

[Marc Huisinga]

By the way, the current minimum VS Code version requirement is 1.75.0 (from January 2023).

[Kevin Sullivan]

Marc Huisinga said:

OK, looking at what happened in 0.0.96, I might have an idea for why you are stuck on such an old version: Your VS Code is probably severely outdated. In 0.0.96 the minimum VS Code version requirement of the extension was bumped to 1.70.0 from 1.61.0. Your VS Code version is probably somewhere between those and VS Code will not update extensions anymore if it does not fulfill the version requirement.

Oh jeez. April 2022 (version 1.67). Yet it seems that I'm constantly accepting offers to update VSCode. I'll just nuke what I have installed and start over again. Thank you very much for this. Wasted multiple hours yesterday on this issue. I'll go give updating a try.

[Marc Huisinga]

If you installed VS Code using a package manager, you may also need to update VS Code using the package manager. I really wish VS Code had informed you about either the fact that your Lean 4 extension version is outdated or that your VS Code updates are failing, though.

[Kevin Sullivan]

Marc Huisinga said:

If you installed VS Code using a package manager, you may also need to update VS Code using the package manager. I really wish VS Code had informed you about either the fact that your Lean 4 extension version is outdated or that your VS Code updates are failing, though.

Thank you, Marc. Updating VSCode worked as expected. Yeah, it was hair-pulling yesterday as I tried everything I could think of to get this all working. Computers!

[Kevin Buzzard]

Out of interest, what are all those funky lean extensions in vscode2.jpg and should I be installing them too?