helloworld

Stream: new members

[Miguel Raz Guzmán Macedo]

Hey all !
I am trying to run my first program in Lean, and the book doesn't have a file extension for a helloworld.
Any recommendations?

[Mario Carneiro]

.lean

[Mario Carneiro]

helloworld.lean:

#eval "hello world"

$ lean helloworld.lean
"hello world"

[Miguel Raz Guzmán Macedo]

helloworld.lean:

#eval "hello world"

$ lean helloworld.lean
"hello world"

yay world has been succesfully hello'd

[Miguel Raz Guzmán Macedo]

How can I download libraries , import, and use them?
What about creating my own? Any guides on becoming a library dev?

[Alex J. Best]

You can find a few useful links at https://github.com/leanprover-community/mathlib/blob/master/README.md

[Alex J. Best]

In particular the first few links will tell you how to add mathlib-tools if you have lean already and then https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md will tell you how to make a new project/library and add mathlib to it. Then it should be sufficient to import topology.basic for instance to start using the stuff in mathlib

[Alex J. Best]

That page gives the example of https://github.com/leanprover-community/lean-perfectoid-spaces which is nice if you want to see how a library is set up, with a leanpkg.toml file and a bunch of lean in the src folder

[Kevin Buzzard]

Do you think that telling beginners (possibly with a CS background) "if you want to clone a project, try this one with an incredibly intimidating name about an incredibly intimidating object" is perhaps a bit...erm...intimidating? Maybe we should make a sample leanprover-community project which has very little, but not nothing, in, e.g. 5 files doing things like the 5 basic problems which Neil Strickland raised a year or so ago, making sure that at least some of them import some mathlib files? I'm talking about this https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package which I think was written when Patrick and Scott and others were organising the big docs push so that newcomers could actually get started without having to come here asking questions about how to even get going.

[Patrick Massot]

I've said countless times I would prefer to mention some version of https://github.com/PatrickMassot/lean-tutorials

[Patrick Massot]

But we got lost in discussion about whether tutorials should be in mathlib or in another place, things like that.

[Patrick Massot]

My opinion is: we should have a leanprover-community hosted tutorial project and refer to it in the docs, and have mathlib CI check it against each new PR.

[vtrandal]

And as one new to leanprover (but not new to the concepts) I am looking for instructions how to install and run leanprover on a trivial example. Does that exist? The Linux build instructions stop short of actually installing leanprover.

[Kevin Buzzard]

The linux build instructions install leanprover in the background I guess, without explicitly mentioning it.

[Kevin Buzzard]

Basically there are currently two possibilities. Try and figure out how to download and compile lean yourself, then try and figure out how to use it, and then try and figure out how to integrate it with an IDE, and then try to figure out how to set up a project. Or alternatively follow the instructions in mathlib's README, so you'll end up with mathlib as well, but you'll also end up with a fully working system with lean and mathlib and VS Code integration.

[vtrandal]

Thanks, Kevin. Where is this mathlib README file?

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib#installation

[vtrandal]

Kevin, thank you. I came here with great enthusiasm after listening to your presentation https://www.youtube.com/watch?v=Dp-mQ3HxgDE
"The Future of Mathematics." Very nice work.

[vtrandal]

Kevin, what is VS Code integration that you mentioned above? Does VS stand for Visual Studio?

[Patrick Massot]

I answered that question in your other thread.

[Patrick Massot]

Yes, it's Visual Studio Code

[vtrandal]

Okay. Visual Studio Code. I had a mental block regarding that for Linux. Makes sense now. Thank you.

[Johan Commelin]

The only alternative is Emacs, if you want interactive Lean

[vtrandal]

Until I get all the details worked out (in Kevin's nice list above) I can use lean online as described here https://leanprover.github.io/reference/using_lean.html#

[vtrandal]

Yes, Johan. Thank you. Locally I can use Lean interactively with Emacs as described here https://leanprover.github.io/reference/using_lean.html#using-lean-with-emacs like you pointed out. Thank you.