lean3 documentation

Stream: general

[Daniel Papp]

Hi!

I would like to find the lean 3 equivalent of https://leanprover.github.io/lean4/doc/ The reason for that is I'm using VS Code to work with this and VS Code only has an extension for lean 3. Could someone link me to a similar doc?

Thanks,
Daniel

[Daniel Papp]

Or is there a way to make lean 4 work alongside VS Code in a similar way as it works in the Natural Number game? That's the only thing I really worked so far.

[Mario Carneiro]

The lean 3 reference manual is probably the nearest equivalent to that page

[Mario Carneiro]

but there is a bunch of documentation from various perspectives that you can find here: https://leanprover-community.github.io/learn.html

[Mario Carneiro]

Lean 4 is still in alpha stage, most of the learning resources haven't been ported yet

[Daniel Papp]

Thanks Mario! I guess the reference manual was the thing I was looking for.

[Bryan Gin-ge Chen]

Note that there is a VS Code extension for lean4, though it's still work in progress: https://github.com/leanprover-community/vscode-lean4

[Daniel Papp]

@Bryan Gin-ge Chen Yep I just tried that. The thing is that it doesn't even provide the basic features like showing the current subgoals as of now.

[Daniel Papp]

I guess I stick with version 3 for the time being.

[Mario Carneiro]

yes, it's not ready for general use yet

[Bryan Gin-ge Chen]

Yeah, there's a lot still missing, though for subgoals you sort of use underscores and the error messages.

[Daniel Papp]

Is version 4 significantly different? Like does it have non backward compatible changes or just extensions to the language?

[Mario Carneiro]

lots of non-backward compatible changes.

[Mario Carneiro]

it's a complete rewrite of lean in lean

[Daniel Papp]

@Bryan Gin-ge Chen Yep but how do I make it show the error messages? I mean with the lean 4 extension.

[Daniel Papp]

@Mario Carneiro Ah I see.

[Bryan Gin-ge Chen]

The error messages show up in the Problems panel: Screen-Shot-2021-01-30-at-6.53.34-PM.png

[Daniel Papp]

Hmm ok, I was expecting something like this in the info window. Let me give it another try using this.

[Daniel Papp]

Btw mathlib is compatible with lean 3 I guess.

[Bryan Gin-ge Chen]

Yeah, the Lean 4 extension doesn't have an info window yet.

[Bryan Gin-ge Chen]

That's right. mathlib uses Lean 3.

[Daniel Papp]

I guess it won't be ported to Lean 4 anytime soon.

[Mario Carneiro]

Discussions about that are under way but I wouldn't expect it before the summer at absolute minimum

[Daniel Papp]

I see.

[Daniel Papp]

Just one more question. Where/How do I download this python script called leanproject?

[Bryan Gin-ge Chen]

You should have gotten it by following your OS-specific instructions on this page: https://leanprover-community.github.io/get_started.html

[Daniel Papp]

Thanks! Why do you use this tool called pipx instead of regular pip to install the package that contains the leanproject command?

[Daniel Papp]

Ah ok actually I can install directly from pip. nvm

[Julian Berman]

pip is essentially a developer tool for developing a package or library, pipx is generally what you'd use for installing a "full application" such as leanproject these days

[Julian Berman]

though at some point I think distributing leanproject as a shiv or zipapp will make things even easier for folks

[Daniel Papp]

I don't know what are the advantages of using such custom solutions when you can add a console_scripts key to entry_points in setup.py like this -> https://python-packaging.readthedocs.io/en/latest/command-line-scripts.html#the-console-scripts-entry-point

But imho creating a statically linked executable with Golang for each supported OS is probably the cleanest solution. You just download it and it works.

[Julian Berman]

pipx is pretty widely used -- what you linked is about specifying how to name binaries (executables) that are installed -- the thing pipx is responsible for is essentially fixing the fact that in Python you should install each application in a separate virtualenv, and doing so manually is tedious when you include making sure the virtualenv's executables are placed on your PATH

[Daniel Papp]

Ah yeah that's true. I use pyenv with 3.7.7 and I just dump everything that I need there without selecting a specific venv since it's already a per user python installation.

[Julian Berman]

Right, that works fine, until it doesn't :), hence pipx.

[Patrick Massot]

Daniel Papp said:

I don't know what are the advantages of using such custom solutions when you can add a console_scripts key to entry_points in setup.py like this -> https://python-packaging.readthedocs.io/en/latest/command-line-scripts.html#the-console-scripts-entry-point

What are you talking about? We do use console scripts entry points. FYI the reason why we started advising people to use pipx is because someone just like you came here without reading any documentation and asking why we were doing everything so stupidly. But it turns out there is nothing we could do to make all those people happy.

[Eric Wieser]

From what I could tell the windows instructions do not mention pipx at all