importing within lean package

Stream: general

[Chris Hughes]

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]

did you do leanpkg init my_project on your directory?

[Chris Hughes]

Which directory?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I don't have a leanpkg path

[Kevin Buzzard]

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]

so you'll need one of those

[Chris Hughes]

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

[Kevin Buzzard]

Mathlib has no dependencies.

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

I'm not sure that's a problem

[Kevin Buzzard]

As long as mathlib compiles

[Chris Hughes]

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

[Simon Hudon]

If you want we can start from scratch.

[Chris Hughes]

It's a problem because it crashes everything

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

type leanpkg upgrade

[Kevin Buzzard]

This should get the correct versions of everything

[Kevin Buzzard]

and then leanpkg build and leave it on overnight

[Kevin Buzzard]

or however long it takes

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Do you have the latest Lean?

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The first error is this:

[Kevin Buzzard]

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

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

[Chris Hughes]

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

[Simon Hudon]

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

[Simon Hudon]

And I use 4ceb545f7e07431263e1131a9c9524a28de99472 for mathlib

[Chris Hughes]

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]

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]

Chris are you able to compile Lean from source?

[Kevin Buzzard]

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

[Simon Hudon]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Kevin Buzzard]

Just google "git change to commit" or something

[Kevin Buzzard]

google is really good for git commands

[Kevin Buzzard]

git checkout commit

[Kevin Buzzard]

is probably how to do it

[Kevin Buzzard]

Oh wooah lean HEAD just failed to build.

[Chris Hughes]

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]

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]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Simon Hudon]

You can get the result of all the builds here:

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

[Simon Hudon]

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]

I don't understand travis.

[Kevin Buzzard]

According to this link:

[Kevin Buzzard]

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

[Kevin Buzzard]

the last successful build was c17e5b913b2db687ab38f53285326b9dbb2b1b6e

[Kevin Buzzard]

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

[Kevin Buzzard]

it was d6d44a19947e2575b3fceed6d61167d258c661fb

[Simon Hudon]

I guess you can try either

[Simon Hudon]

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]

That's a good idea.

[Kevin Buzzard]

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

[Simon Hudon]

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]

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]

(deleted)