Zulip Chat Archive

Stream: general

Topic: Missing some set theorems?


view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 25 2018 at 03:39):

It got renamed recently to data.set.basic

view this post on Zulip Simon Hudon (Jul 25 2018 at 03:40):

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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 03:41):

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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 03:41):

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

view this post on Zulip 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?

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 03:44):

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"

view this post on Zulip 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.

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 03:46):

What should I add to the leanpkg.toml file?

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 03:47):

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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:15):

Sorry i stepped away

view this post on Zulip 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)

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:16):

Then call leanpkg add leanprover/mathlib

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:16):

then leanpkg build

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:17):

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

view this post on Zulip 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'

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:24):

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

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:26):

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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:26):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:37):

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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:39):

Yeah, "no definition found for univ"

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:39):

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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:39):

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

view this post on Zulip 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!

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:40):

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

view this post on Zulip 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

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:40):

Lean version 3.3.0

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:44):

Yes, that makes things much easier

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:47):

Got it, thanks!

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:47):

Maybe we should remove it from homebrew and put elan instead

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 04:54):

OK, good point

view this post on Zulip Simon Hudon (Jul 25 2018 at 04:54):

Any luck with elan so far?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 15:58):

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

view this post on Zulip Reid Barton (Jul 25 2018 at 15:58):

You need some version of leanpkg add

view this post on Zulip Reid Barton (Jul 25 2018 at 15:59):

Which will add to that dependencies section for you.

view this post on Zulip Reid Barton (Jul 25 2018 at 16:01):

(or you can edit that section manually)

view this post on Zulip Lyle Kopnicky (Jul 25 2018 at 16:01):

Ah, that seemed to do the trick. Thanks!

view this post on Zulip Reid Barton (Jul 25 2018 at 16:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 19:01):

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

view this post on Zulip 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.

view this post on Zulip 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