Opening my first lean project

Stream: new members

[Choink Ivt]

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?

[Johan Commelin]

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

[Johan Commelin]

Fixed the link

[Johan Commelin]

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

[Johan Commelin]

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

[Choink Ivt]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Maybe VScode updated their color styles...

[Choink Ivt]

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

[Johan Commelin]

Ok, so Lean is working

[Johan Commelin]

Sorry, I need to run

[Johan Commelin]

You need to use leanpkg to start a project

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I really need to go, maybe someone else can help

[Choink Ivt]

Ah that seems to be the missing step. Thanks!

[Patrick Massot]

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

[Choink Ivt]

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/?

[Patrick Massot]

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

[Choink Ivt]

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

[Marc Huisinga]

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

[Choink Ivt]

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.

[Patrick Massot]

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.

[Patrick Massot]

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

[Choink Ivt]

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

[Kevin Buzzard]

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

[Liam]

Hello,
As a project manager, I found Lean.io potentially very useful for my dev team. After reviewing a youtube video about "Lean GUI" something was mentioned about a membership.
Can someone answer these questions and provide their associated resource?

1. Is Lean.io totally free for commercial use and project development?
2. If my team uses Lean.io, does my project keep all IPs (Intellectual Property)?
3. Does Lean.io include an electronic trading interface?

Thank you.

[Mauricio Collares]

That's a different Lean, sorry :( This Zulip instance is used for the Lean theorem prover (leanprover.github.io).

[Liam]

oh okay, thank you very much for the support. Do you know where I could find answers to these questions at all?

[Mauricio Collares]

https://www.quantconnect.com/forum/discussions/1/lean would be my guess

[Mauricio Collares]

They have a Discord too

[Liam]

I tried both the discord link doesn't connect me and I need to go through some BootCamp to even post a comment in the community

[Liam]

Thank you very much for taking the time to help. I don't know a lot about coding I am just trying to support my developers as best I can

[Mauricio Collares]

The Discord invite link on the website is https://discord.com/invite/PT7aBN2nkY, if that helps. They have a Lean channel. Good luck!

[Liam]

I am going to try another web browser chrome doesn't seem to be bringing up the right discord server. Thank you for the help