Zulip Chat Archive

Stream: new members

Topic: Opening my first lean project


view this post on Zulip Choink Ivt (Oct 03 2019 at 08:20):

Hello, I'm trying to follow the instructions on https://xenaproject.wordpress.com/installing-lean-and-mathlib/ but it says

If you want Lean and mathlib to work on a local installation, you need to open a project. You can tell when a folder contains a Lean project because the folder will have a file called leanpkg.path and another file called leanpkg.toml in it.

I don't have any projects and I can't find a way to create one, and trying to run import data.int.basic without a project gives me the error of neading to install leanpkg.path. How can I solve this issue?

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:24):

Hi @Choink Ivt, do these instructions help: https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:24):

Fixed the link

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:25):

@Kevin Buzzard Can you update that blogpost to point towards the installation instructions in https://github.com/leanprover-community/mathlib/blob/master/README.md

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:26):

@Choink Ivt In that directory there is a bunch of installation instructions depending on OS: Linux/Mac/Windows, etc...

view this post on Zulip Choink Ivt (Oct 03 2019 at 08:28):

Hi @Johan Commelin! When I type #eval 1+1 I get a blue squiggly line, not a green one, but 2 appears in Lean Messages - is that intended? I'm using https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md, and have installed mathlib, elan and VS Code.

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:33):

What happens if you type #check nat and/or #check 3?

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:34):

If those give output Type resp. nat, then I wouldn't be too concerned.

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:34):

Maybe VScode updated their color styles...

view this post on Zulip Choink Ivt (Oct 03 2019 at 08:34):

I get N: Type and 3: N (with blackboard style N). But the import data.int.basic is still showing 2 errors.

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:36):

Ok, so Lean is working

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:38):

Sorry, I need to run

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:39):

You need to use leanpkg to start a project

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:39):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:40):

This doesn't seem to be mentioned in the Windows install instructions...

view this post on Zulip Johan Commelin (Oct 03 2019 at 08:40):

I really need to go, maybe someone else can help

view this post on Zulip Choink Ivt (Oct 03 2019 at 08:40):

Ah that seems to be the missing step. Thanks!

view this post on Zulip Patrick Massot (Oct 03 2019 at 09:07):

The last line of https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md is a link to https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md, which is common to all OS

view this post on Zulip Choink Ivt (Oct 03 2019 at 09:34):

Ah thanks, must have missed that. It's working now, though it's taking a long time to check the packages. Are there any recommended ways to get started, or should I just float around the various sites such as https://xenaproject.wordpress.com/ and http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html/?

view this post on Zulip Patrick Massot (Oct 03 2019 at 09:55):

It shouldn't take a long time. Did you run update-mathlib in your project?

view this post on Zulip Choink Ivt (Oct 03 2019 at 10:06):

Yep. I just opened it again and it was a lot quicker this time; perhaps something was running in the background.

view this post on Zulip Marc Huisinga (Oct 03 2019 at 10:21):

TPIL (https://leanprover.github.io/theorem_proving_in_lean/) is a great introduction that covers the basics of lean itself.

view this post on Zulip Choink Ivt (Oct 03 2019 at 11:19):

I'm trying to work through https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/; I'm trying to prove a=b given a+zero=b+zero, but I don't understand why rw [←add_zero] is not changing this to a+zero=b (perhaps with +zero on the end), since add_zero is the statement n+zero=n.

view this post on Zulip Patrick Massot (Oct 03 2019 at 11:45):

Could you please post some code that we could run on our end? This would make it much more likely that you'll receive help.

view this post on Zulip Patrick Massot (Oct 03 2019 at 11:46):

It is very hard to know what you did wrong with so few information.

view this post on Zulip Choink Ivt (Oct 03 2019 at 12:12):

I would but I discovered a workaround that finished the proof, thanks anyway.

view this post on Zulip Kevin Buzzard (Oct 03 2019 at 15:53):

There was a direct link from the home page which I've now moved to point to the installation part of the readme. Thanks for pointing this out @Johan Commelin


Last updated: May 07 2021 at 00:30 UTC