Open Documentation View

Stream: lean4

[Alistair Tucker]

Hi I asked about this in the new members stream but got no reply. Basically I can't find how to open TPIL4 in VS Code. Any ideas?

[Edward Ayers]

I'm not completely sure this is what you want, but you can clone the source repository at https://github.com/leanprover/theorem_proving_in_lean4. There are no lean files per se, instead the lean is in the markdown files. The readme gives some instructions for testing all of the lean code blocks in the command line. If you are after the 'try it!' functionality where you can quickly run code blocks in Lean I think that is still tbd.

[Alistair Tucker]

Thanks! I'll try that. I read about "Try it!" in the introduction and thought it was already working

[Edward Ayers]

If your goal is to learn about Lean 4 then your best bet is to read TPIL4 online and the lean 4 manual. All the learning resources for Lean 4 are WIP.

[Edward Ayers]

The learning resources for Lean 3 are mature so if you are learning about theorem proving for the first time it might be better to use Lean 3.

[Wojciech Nawrocki]

Oh, that's a bug in the extension. I filed it at leanprover/vscode-lean4#185.

[Edward Ayers]

Ahh sorry my bad I assumed it wasn't working yet.

[Chris Lovett]

it's fixed now in Lean extension 0.0.77:
image.png

[Yuri de Wit]

This is quite helpful, thank you!

@Chris Lovett this caught my attention:

Note: Packages have to be opened using "File > Open Folder..." for imports to work. Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (Ctrl+Shift+X).

What is meant by a package here? A external project or an internal module in a sub-folder? I ask because I was seeing a strange error trying to import a module in a sub-folder in my lake-based project. I will see if I can reproduce the same error message.

[Chris Lovett]

Ah, it means Lake packages - folders initialized using Lake init :

lake init --help
Create a Lean package in the current directory

USAGE:
  lake init <name>

This command creates a new Lean package with the given name in
the current directory.

but the quickstart doc page should also say that vscode workspaces also works.

[Yuri de Wit]

Gosh, just realized I replied in the wrong thread ...