## Stream: general

### Topic: Missing some set theorems?

#### Lyle Kopnicky (Jul 25 2018 at 03:32):

Hi folks, I have been following Logic & Proof (https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf) and in Chapter 12, it says to use import data.set, but I get an error that that path doesn't exist. However, I am still able to use set membership operators, etc. On the other hand, the book mentions theorems like mem_inter, but those aren't in scope. Have they moved to another library? How do I import them? Thanks.

#### Simon Hudon (Jul 25 2018 at 03:39):

It got renamed recently to data.set.basic

#### Simon Hudon (Jul 25 2018 at 03:40):

@Mario Carneiro @Jeremy Avigad This would be worth updating I believe

#### Lyle Kopnicky (Jul 25 2018 at 03:41):

Ah, thanks, that doesn't seem to work either. Maybe my Lean installation is old.

#### Lyle Kopnicky (Jul 25 2018 at 03:41):

I'm using the Lean extension in VS Code, also.

#### Simon Hudon (Jul 25 2018 at 03:42):

Can you bring up your project's leanpkg.toml and check that you have mathlib in your dependencies?

Yeah, I don't seem to have that. It's in $HOME/lean-3.3.0-darwin/lib/lean/leanpkg/leanpkg.toml and it just has: [package] name = "leanpkg" version = "0.1"  #### Lyle Kopnicky (Jul 25 2018 at 03:45): I guess that's a global leanpkg.toml file? I don't have one for my project. I'm just creating individual .lean files. #### Lyle Kopnicky (Jul 25 2018 at 03:46): What should I add to the leanpkg.toml file? #### Lyle Kopnicky (Jul 25 2018 at 03:47): Or maybe I need to run the leanpkg command to add a library? #### Lyle Kopnicky (Jul 25 2018 at 03:49): I really know nothing about lean package management. Just did the minimal amount to get Lean and the VS Code extension installed. #### Simon Hudon (Jul 25 2018 at 04:15): Sorry i stepped away #### Simon Hudon (Jul 25 2018 at 04:16): go in your project's directory with a terminal and call leanpkg init my_project (feel free to pick a better name) #### Simon Hudon (Jul 25 2018 at 04:16): Then call leanpkg add leanprover/mathlib #### Simon Hudon (Jul 25 2018 at 04:16): then leanpkg build #### Simon Hudon (Jul 25 2018 at 04:17): By default, leanpkg sets src as the directory where all your sources are located #### Lyle Kopnicky (Jul 25 2018 at 04:22): Thanks! The leanpkg init my_project worked, but: $ leanpkg add leanprover/mathlib
mathlib: using local path ./leanprover/mathlib
failed to open file './leanprover/mathlib/leanpkg.toml'


#### Simon Hudon (Jul 25 2018 at 04:24):

sometimes you have to be more explicit: leanpkg add https://github.com/leanprover/mathlib

#### Simon Hudon (Jul 25 2018 at 04:26):

Btw, this might help: https://github.com/leanprover/mathlib/blob/master/docs/elan.md

#### Lyle Kopnicky (Jul 25 2018 at 04:26):

That add command seemed to work, thanks. I'm doing the build.

#### Lyle Kopnicky (Jul 25 2018 at 04:27):

It's funny, I just recently added a similar feature to the Haskell build tool Stack, to be able to download templates from different github users without having to specify the full path.

#### Lyle Kopnicky (Jul 25 2018 at 04:29):

The Elan tool looks helpful, thanks. Sounds a bit like Stack actually, letting you use different versions of the compiler.

#### Lyle Kopnicky (Jul 25 2018 at 04:33):

Well, the leanpkg build ran successfully. And I restarted the editor, and now the import data.set.basic shows no error. But univ, mem_inter, and those other theorems are still redlined. Maybe I need to open some namespace?

#### Simon Hudon (Jul 25 2018 at 04:35):

To be fair elan and leanpkg share some the functions of stack but we still don't have curated package collections.

#### Simon Hudon (Jul 25 2018 at 04:35):

Wasn't it already possible to link to github in your stack.yaml file, in the packages section?

#### Lyle Kopnicky (Jul 25 2018 at 04:35):

Ah, right. Well that's a pretty unique feature to stack.

#### Simon Hudon (Jul 25 2018 at 04:36):

I'm hoping to see that happen eventually. I find it pretty useful. But mathlib changes so much that we keep upgrading.

#### Lyle Kopnicky (Jul 25 2018 at 04:37):

This is about templates for new projects. There's a set of templates under the commercialstack user on github. This was so you could install templates from a different github user by writing stack new username/template_name. Instead of having to write the whole URL.

#### Simon Hudon (Jul 25 2018 at 04:37):

In VS code, there may be a command to let you find definitions.

#### Lyle Kopnicky (Jul 25 2018 at 04:39):

Yeah, "no definition found for univ"

#### Simon Hudon (Jul 25 2018 at 04:39):

I might have misled you. Try also importing data.set

#### Lyle Kopnicky (Jul 25 2018 at 04:39):

OK, added that. Still can't find univ.

#### Simon Hudon (Jul 25 2018 at 04:39):

This is about templates for new projects. There's a set of templates under the commercialstack user on github. This was so you could install templates from a different github user by writing stack new username/template_name. Instead of having to write the whole URL.

Nice!

#### Simon Hudon (Jul 25 2018 at 04:40):

What version of Lean is written in your leanpkg.toml?

#### Lyle Kopnicky (Jul 25 2018 at 04:40):

You can also install templates from gitlab or bitbucket, e.g. stack new gitlab:username/template_name

#### Lyle Kopnicky (Jul 25 2018 at 04:40):

Lean version 3.3.0

#### Simon Hudon (Jul 25 2018 at 04:41):

Ok, that makes sense. Let's set it to 3.4.1 to have the most recent stuff.

#### Lyle Kopnicky (Jul 25 2018 at 04:42):

OK, I changed it and ran leanpkg build but got the error WARNING: Lean version mismatch: installed version is 3.3.0, but package requires 3.4.1 . Maybe I need to install elan.

#### Simon Hudon (Jul 25 2018 at 04:44):

Yes, that makes things much easier

#### Lyle Kopnicky (Jul 25 2018 at 04:45):

Thing is, I'm leading a study group tomorrow night where we're supposed to go over the exercises for Chapter 12. And I just got around to working on them tonight, and now I realize probably nobody else is going to be able to work them either. Will have to post instructions for folks.

#### Simon Hudon (Jul 25 2018 at 04:47):

That would be good. I think this might be a good start: https://github.com/leanprover/mathlib/blob/master/docs/elan.md

#### Lyle Kopnicky (Jul 25 2018 at 04:47):

I wonder how I installed Lean the first time - probably just downloaded the binary package. Looks like it's on homebrew and that has 3.4.1 - might have been another simple way to keep it up to date.

Got it, thanks!

#### Simon Hudon (Jul 25 2018 at 04:47):

Maybe we should remove it from homebrew and put elan instead

#### Lyle Kopnicky (Jul 25 2018 at 04:49):

Nah. Both ghc and stack are on homebrew. People can choose what they want. But it would be helpful if this page said anything about elan: https://leanprover.github.io/download/

#### Simon Hudon (Jul 25 2018 at 04:52):

Yeah that's true. The thing with ghc though is that there are many options for build systems. Some people use cabal, others nix. But with Lean, I think it's too easy to get started the wrong way and there aren't that many different ways of using the tool.

OK, good point

#### Simon Hudon (Jul 25 2018 at 04:54):

Any luck with elan so far?

#### Simon Hudon (Jul 25 2018 at 04:59):

I should go, my bed is calling to me. I hope it works out for your study session

#### Lyle Kopnicky (Jul 25 2018 at 05:12):

Sorry, just biked home because the coffee shop closed. Will try elan now. Thanks and take care.

#### Mario Carneiro (Jul 25 2018 at 07:45):

@Lyle Kopnicky I think the missing step is open set. Assuming you got import data.set.basic working, the name of the univ set is set.univ or just univ if set is open.

#### Lyle Kopnicky (Jul 25 2018 at 15:56):

Thanks @Mario Carneiro, but I am even further back now. I installed Elan and did leanpkg install leanprover/mathlib and that seemed to work fine. Then did leanpkg build and it crashed with <unknown>:1:1: error: file 'data/list/basic' not found in the LEAN_PATH. How do I install that? I tried leanpkg install data/list/basic but it says that path is not found.

#### Lyle Kopnicky (Jul 25 2018 at 15:57):

Here is my leanpkg.toml:

[package]
name = "logic_and_proof"
version = "0.1"
lean_version = "3.4.1"

[dependencies]


Do I need to manually add something to dependencies?

#### Lyle Kopnicky (Jul 25 2018 at 15:58):

I though running leanpkg install leanprover/mathlib would add something to dependencies but it didn't.

#### Reid Barton (Jul 25 2018 at 15:58):

You need some version of leanpkg add

#### Reid Barton (Jul 25 2018 at 15:59):

Which will add to that dependencies section for you.

#### Reid Barton (Jul 25 2018 at 16:01):

(or you can edit that section manually)

#### Lyle Kopnicky (Jul 25 2018 at 16:01):

Ah, that seemed to do the trick. Thanks!

#### Reid Barton (Jul 25 2018 at 16:02):

leanpkg install is analogous to cabal install I think. Not sure I have ever used it.

#### Lyle Kopnicky (Jul 25 2018 at 16:03):

OK. Up until yesterday I hadn't used leanpkg at all. Have just been using individual .lean files but that didn't work anymore when I needed some of these set theorems.

#### Lyle Kopnicky (Jul 25 2018 at 18:58):

Yay, finally have it working, following the leanpkg build. In the code, import data.set followed by open set works.

#### Kevin Buzzard (Jul 25 2018 at 19:01):

How many seconds have you now got to do all the exercises? :-)

#### Lyle Kopnicky (Jul 27 2018 at 03:17):

Haha... I didn't manage to do the exercise beforehand. But others in the group did, so they presented their solutions. It was awesome. One person had already installed Elan, I guess, and another was using the online Lean, so they were both able to do the exercises.

#### Lyle Kopnicky (Jul 27 2018 at 03:18):

But during the meeting, I was able to paste their code into my editor and everything checked out fine. I was projecting it on the whiteboard and they could underline things and draw around them.

Last updated: May 08 2021 at 05:14 UTC