Stream: new members
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.
Mario Carneiro (Oct 11 2019 at 02:46):
Mario Carneiro (Oct 11 2019 at 02:47):
#eval "hello world"
$ lean helloworld.lean "hello world"
Miguel Raz Guzmán Macedo (Oct 11 2019 at 02:54):
helloworld.lean:#eval "hello world"
$ lean helloworld.lean
yay world has been succesfully hello'd
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?
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
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
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
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.
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
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.
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.
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.
Kevin Buzzard (Oct 11 2019 at 09:47):
The linux build instructions install leanprover in the background I guess, without explicitly mentioning it.
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.
vtrandal (Oct 11 2019 at 09:58):
Thanks, Kevin. Where is this mathlib README file?
Kevin Buzzard (Oct 11 2019 at 10:12):
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.
vtrandal (Oct 11 2019 at 10:55):
Kevin, what is VS Code integration that you mentioned above? Does VS stand for Visual Studio?
Patrick Massot (Oct 11 2019 at 10:56):
I answered that question in your other thread.
Patrick Massot (Oct 11 2019 at 10:56):
Yes, it's Visual Studio Code
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.
Johan Commelin (Oct 11 2019 at 11:41):
The only alternative is Emacs, if you want interactive Lean
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#
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