Zulip Chat Archive

Stream: new members

Topic: helloworld


view this post on Zulip Miguel Raz Guzmán Macedo (Oct 11 2019 at 02:46):

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?

view this post on Zulip Mario Carneiro (Oct 11 2019 at 02:46):

.lean

view this post on Zulip Mario Carneiro (Oct 11 2019 at 02:47):

helloworld.lean:

#eval "hello world"
$ lean helloworld.lean
"hello world"

view this post on Zulip Miguel Raz Guzmán Macedo (Oct 11 2019 at 02:54):

helloworld.lean:

#eval "hello world"

$ lean helloworld.lean
"hello world"


yay world has been succesfully hello'd

view this post on Zulip Miguel Raz Guzmán Macedo (Oct 11 2019 at 04:08):

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

view this post on Zulip Alex J. Best (Oct 11 2019 at 04:12):

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

view this post on Zulip Alex J. Best (Oct 11 2019 at 04:15):

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

view this post on Zulip Alex J. Best (Oct 11 2019 at 04:18):

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

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 07:30):

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.

view this post on Zulip Patrick Massot (Oct 11 2019 at 08:22):

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

view this post on Zulip Patrick Massot (Oct 11 2019 at 08:23):

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

view this post on Zulip Patrick Massot (Oct 11 2019 at 08:24):

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.

view this post on Zulip vtrandal (Oct 11 2019 at 09:28):

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.

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 09:47):

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

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 09:48):

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.

view this post on Zulip vtrandal (Oct 11 2019 at 09:58):

Thanks, Kevin. Where is this mathlib README file?

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 10:12):

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

view this post on Zulip vtrandal (Oct 11 2019 at 10:38):

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.

view this post on Zulip vtrandal (Oct 11 2019 at 10:55):

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

view this post on Zulip Patrick Massot (Oct 11 2019 at 10:56):

I answered that question in your other thread.

view this post on Zulip Patrick Massot (Oct 11 2019 at 10:56):

Yes, it's Visual Studio Code

view this post on Zulip vtrandal (Oct 11 2019 at 11:40):

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

view this post on Zulip Johan Commelin (Oct 11 2019 at 11:41):

The only alternative is Emacs, if you want interactive Lean

view this post on Zulip vtrandal (Oct 11 2019 at 11:49):

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#

view this post on Zulip vtrandal (Oct 11 2019 at 12:00):

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.


Last updated: May 08 2021 at 19:11 UTC