Zulip Chat Archive

Stream: general

Topic: importing within lean package


Chris Hughes (Mar 24 2018 at 20:09):

So I've tried to download @Kenny Lau and @Kevin Buzzard's stacks project library, but none of the imports are currently working, I get the following message

invalid import: Kenny_comm_alg.avoid_powers
could not resolve import: Kenny_comm_alg.avoid_powers

I tried using both leanpkg install and leanpkg add to download the library, but both have this problem. I'm on windows. Can anyone help?

Simon Hudon (Mar 24 2018 at 20:10):

did you do leanpkg init my_project on your directory?

Chris Hughes (Mar 24 2018 at 20:12):

Which directory?

Kevin Buzzard (Mar 24 2018 at 20:15):

Chris : try the "open folder" option in VS Code. Open the project root as a folder.

Kevin Buzzard (Mar 24 2018 at 20:15):

Let me know if it doesn't work. I'll add it to the README if it does.

Kevin Buzzard (Mar 24 2018 at 20:16):

That should make the import directories all point to the right places

Kevin Buzzard (Mar 24 2018 at 20:18):

and then I would have suggested "leanpkg upgrade" or "leanpkg build" -- oh -- I see -- this doesn't work because Chris won't have any leanpkg.path file in his clone?

Chris Hughes (Mar 24 2018 at 20:19):

I don't have a leanpkg path

Kevin Buzzard (Mar 24 2018 at 20:19):

Chris -- I have a _target directoy that you don't have because my gitignore file tells git not to upload my _target directory to github

Kevin Buzzard (Mar 24 2018 at 20:19):

so you'll need one of those

Chris Hughes (Mar 24 2018 at 20:19):

But I should be able to build it, I can build mathlib, and that's the same.

Kevin Buzzard (Mar 24 2018 at 20:20):

Mathlib has no dependencies.

Kevin Buzzard (Mar 24 2018 at 20:20):

Our project depends on other projects so it's a bit different.

Chris Hughes (Mar 24 2018 at 20:20):

It downloaded all the dependecncies automatically. Trouble is they don't compile.

Kevin Buzzard (Mar 24 2018 at 20:20):

I'm not sure that's a problem

Kevin Buzzard (Mar 24 2018 at 20:21):

As long as mathlib compiles

Chris Hughes (Mar 24 2018 at 20:21):

And my computer's too slow to make compiling when I import practical.

Simon Hudon (Mar 24 2018 at 20:22):

If you want we can start from scratch.

Chris Hughes (Mar 24 2018 at 20:22):

It's a problem because it crashes everything

Kevin Buzzard (Mar 24 2018 at 20:22):

You should be able to get it to work. Kenny got it to work

Chris Hughes (Mar 24 2018 at 20:22):

And I doubt mathlib compileseither, since it depends on an old version

Kevin Buzzard (Mar 24 2018 at 20:22):

and he was in exactly the same situation as you -- it wasn't his project and he had to clone from github

Kevin Buzzard (Mar 24 2018 at 20:23):

type leanpkg upgrade

Kevin Buzzard (Mar 24 2018 at 20:23):

This should get the correct versions of everything

Kevin Buzzard (Mar 24 2018 at 20:23):

and then leanpkg build and leave it on overnight

Kevin Buzzard (Mar 24 2018 at 20:23):

or however long it takes

Chris Hughes (Mar 24 2018 at 20:24):

If there are errors, leaving it overnight doesn't help

Kevin Buzzard (Mar 24 2018 at 20:26):

You're right, it's not working for me.

Kevin Buzzard (Mar 24 2018 at 20:26):

I'll try and figure out what's going on.

Kevin Buzzard (Mar 24 2018 at 20:27):

Do you have the latest Lean?

Chris Hughes (Mar 24 2018 at 20:28):

The latest lean doesn't compile. I have four day old lean.

Kevin Buzzard (Mar 24 2018 at 20:37):

OK so I just tried compiling my project using lean from the linux nightly (commit 28f4143be31b) and my project did not compile.

Kevin Buzzard (Mar 24 2018 at 20:37):

The first error is this:

Kevin Buzzard (Mar 24 2018 at 20:37):

/home/buzzard/temp/lean-stacks-project/_target/deps/mathlib/data/option.lean:24:1: error: failed to synthesize type class instance for
α : Type u
⊢ is_lawful_monad option

Kevin Buzzard (Mar 24 2018 at 20:38):

and there was some talk about lawful monads recently so maybe there was some change

Chris Hughes (Mar 24 2018 at 20:41):

If you just find a version it works with, I'll download that.

Simon Hudon (Mar 24 2018 at 20:42):

I believe mathlib doesn't build with the latest nightly. I worked with revision 07bb7d809b6be49f38ce4e427c54a82708ae281f of Lean

Simon Hudon (Mar 24 2018 at 20:43):

And I use 4ceb545f7e07431263e1131a9c9524a28de99472 for mathlib

Chris Hughes (Mar 24 2018 at 20:45):

I have made some progress. It now gets stuck at importing, because nothing's compiled instead of not finding the file it's meant to import.

Kevin Buzzard (Mar 24 2018 at 20:46):

I am downloading lean HEAD. It's three days old and it would not surprise me if ever-efficient Mario had made mathlib work with it.

Kevin Buzzard (Mar 24 2018 at 20:46):

Chris are you able to compile Lean from source?

Kevin Buzzard (Mar 24 2018 at 20:46):

https://github.com/leanprover/lean/blob/master/doc/make/msys2.md

Simon Hudon (Mar 24 2018 at 20:46):

If you check travis, you'll see that it doesn't work with HEAD

Chris Hughes (Mar 24 2018 at 20:47):

Probably not with the current version, since it says build failing. Maybe with a previous version.

Chris Hughes (Mar 24 2018 at 20:47):

But I haven't worked out how to build an old commit with git yet.

Kevin Buzzard (Mar 24 2018 at 20:49):

Just google "git change to commit" or something

Kevin Buzzard (Mar 24 2018 at 20:50):

google is really good for git commands

Kevin Buzzard (Mar 24 2018 at 20:50):

git checkout commit

Kevin Buzzard (Mar 24 2018 at 20:50):

is probably how to do it

Kevin Buzzard (Mar 24 2018 at 20:50):

Oh wooah lean HEAD just failed to build.

Chris Hughes (Mar 24 2018 at 20:55):

Yeah. If we just find a version of lean and mathlib to use it should be fine. But I don't know which version.

Simon Hudon (Mar 24 2018 at 20:56):

Simon Hudon: I believe mathlib doesn't build with the latest nightly. I work with revision 07bb7d809b6be49f38ce4e427c54a82708ae281f  of Lean

Simon Hudon: And I use 4ceb545f7e07431263e1131a9c9524a28de99472 for mathlib

Kevin Buzzard (Mar 24 2018 at 20:56):

I just checked out c4cc8c88c08d86cd902c577de09ef69528c2da36 of Lean on the basis that it was the most recent version that compiled (as far as I coudl see)

Mario Carneiro (Mar 24 2018 at 20:58):

I built a version slightly in advance of the nightly, but it should be out now

Chris Hughes (Mar 24 2018 at 21:01):

Where are the instructions on building lean? I did it before, but I don't remember how

Kevin Buzzard (Mar 24 2018 at 21:02):

Do you know which commit it works with? I am having trouble getting Lean to compile from source and mathlib doesn't compile if I download the latest linux nightly and then use "leanpkg upgrade"

Kevin Buzzard (Mar 24 2018 at 21:03):

Where are the instructions on building lean? I did it before, but I don't remember how

https://github.com/leanprover/lean/blob/master/doc/make/msys2.md

Chris Hughes (Mar 24 2018 at 21:05):

I''ve been using the f7977ff5a6bcf7e5c54eec908364ceb40dafc795 version of mathlib. The latest version only works with the version of lean that doesn't work

Kevin Buzzard (Mar 24 2018 at 21:07):

How do I get travis to tell me the last Lean commit which compiled for linux?

Kevin Buzzard (Mar 24 2018 at 21:07):

And how do I get mathlib to tell me the version of Lean which it compiled against?

Simon Hudon (Mar 24 2018 at 21:09):

You can get the result of all the builds here:

https://travis-ci.org/leanprover/mathlib/builds

Simon Hudon (Mar 24 2018 at 21:11):

I'm not sure how to use that to infer the corresponding version of Lean other than see that the last successful build was 10 days ago. We can go and see what version Lean was on 10 days ago

Kevin Buzzard (Mar 24 2018 at 21:12):

I don't understand travis.

Kevin Buzzard (Mar 24 2018 at 21:12):

According to this link:

Kevin Buzzard (Mar 24 2018 at 21:12):

https://ci.appveyor.com/project/leodemoura/lean/history

Kevin Buzzard (Mar 24 2018 at 21:12):

the last successful build was c17e5b913b2db687ab38f53285326b9dbb2b1b6e

Kevin Buzzard (Mar 24 2018 at 21:13):

but according to https://travis-ci.org/leanprover/lean/builds

Kevin Buzzard (Mar 24 2018 at 21:14):

it was d6d44a19947e2575b3fceed6d61167d258c661fb

Simon Hudon (Mar 24 2018 at 21:15):

I guess you can try either

Simon Hudon (Mar 24 2018 at 21:16):

You might be interested in recording the version of Lean that you use in your repository. You can facilitate the testing and importing this way

Kevin Buzzard (Mar 24 2018 at 21:29):

That's a good idea.

Kevin Buzzard (Mar 24 2018 at 21:30):

If I decide to use leanpkg upgrade with a specific version of lean, which version of mathlib will it upgrade to?

Simon Hudon (Mar 24 2018 at 21:30):

If you need a reference, I have some scripts for that. Some of them blocks you from committing on git if your lean version is inaccurate

Simon Hudon (Mar 24 2018 at 21:31):

I think there are two possibilities: if you're on an official release (say 3.3.0) it will get the version of mathlib that works with it. Otherwise, it will get HEAD

Kevin Buzzard (Mar 24 2018 at 21:41):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC