Missing some set theorems?

Stream: general

[Lyle Kopnicky]

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]

It got renamed recently to data.set.basic

[Simon Hudon]

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

[Lyle Kopnicky]

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

[Lyle Kopnicky]

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

[Simon Hudon]

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

[Lyle Kopnicky]

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]

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]

What should I add to the leanpkg.toml file?

[Lyle Kopnicky]

Or maybe I need to run the leanpkg command to add a library?

[Lyle Kopnicky]

I really know nothing about lean package management. Just did the minimal amount to get Lean and the VS Code extension installed.

[Simon Hudon]

Sorry i stepped away

[Simon Hudon]

go in your project's directory with a terminal and call leanpkg init my_project (feel free to pick a better name)

[Simon Hudon]

Then call leanpkg add leanprover/mathlib

[Simon Hudon]

then leanpkg build

[Simon Hudon]

By default, leanpkg sets src as the directory where all your sources are located

[Lyle Kopnicky]

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]

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

[Simon Hudon]

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

[Lyle Kopnicky]

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

[Lyle Kopnicky]

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]

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

[Lyle Kopnicky]

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]

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

[Simon Hudon]

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

[Lyle Kopnicky]

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

[Simon Hudon]

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

[Lyle Kopnicky]

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]

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

[Lyle Kopnicky]

Yeah, "no definition found for univ"

[Simon Hudon]

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

[Lyle Kopnicky]

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

[Simon Hudon]

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]

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

[Lyle Kopnicky]

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

[Lyle Kopnicky]

Lean version 3.3.0

[Simon Hudon]

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

[Lyle Kopnicky]

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]

Yes, that makes things much easier

[Lyle Kopnicky]

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]

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

[Lyle Kopnicky]

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.

[Lyle Kopnicky]

Got it, thanks!

[Simon Hudon]

Maybe we should remove it from homebrew and put elan instead

[Lyle Kopnicky]

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]

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.

[Lyle Kopnicky]

OK, good point

[Simon Hudon]

Any luck with elan so far?

[Simon Hudon]

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

[Lyle Kopnicky]

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

[Mario Carneiro]

@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]

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]

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]

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

[Reid Barton]

You need some version of leanpkg add

[Reid Barton]

Which will add to that dependencies section for you.

[Reid Barton]

(or you can edit that section manually)

[Lyle Kopnicky]

Ah, that seemed to do the trick. Thanks!

[Reid Barton]

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

[Lyle Kopnicky]

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]

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

[Kevin Buzzard]

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

[Lyle Kopnicky]

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]

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.