leanproject issues with add-mathlib/update-mathlib

Stream: general

[Ryan Lahfa]

For some reason, maybe I'm doing something wrong but leanproject update-mathlib does not update the mathlib, when I try to do new, it does not pick up the files in src/ and says the project does not depend on mathlib.

Also, I don't know how feasible it is to say to leanproject to use my own .git (the root one) rather than doing the Git management for me.

Here's the repository: https://github.com/RaitoBezarius/projet-maths-lean/tree/master/espaces-metriques (there are a lot of things to say regarding the code… but that will be for another day! :D)

[Ryan Lahfa]

FWIW, I'm using mathlibtools-0.0.4

[Kevin Buzzard]

What happens if you type leanproject up in the root directory? Note that leanproject does not support lean repositories that are not git repositories

[Ryan Lahfa]

Kevin Buzzard said:

What happens if you type leanproject up in the root directory? Note that leanproject does not support lean repositories that are not git repositories

It's a git repository technically, just I don't want the .git to be in the project folder, maybe it's a limitation of leanproject though.

[Ryan Lahfa]

Kevin Buzzard said:

What happens if you type leanproject up in the root directory? Note that leanproject does not support lean repositories that are not git repositories

mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 230, done.
remote: Counting objects: 100% (230/230), done.
remote: Compressing objects: 100% (151/151), done.
remote: Total 40939 (delta 120), reused 127 (delta 76), pack-reused 40709
Receiving objects: 100% (40939/40939), 19.85 MiB | 12.06 MiB/s, done.
Resolving deltas: 100% (31222/31222), done.
> git checkout --detach 906874e2f337e78235d81e27f01f25152846e392    # in directory _target/deps/mathlib
HEAD is now at 906874e2 feat(category_theory): quotient categories (#2310)
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: trying to update _target/deps/mathlib to revision 906874e2f337e78235d81e27f01f25152846e392
> git checkout --detach 906874e2f337e78235d81e27f01f25152846e392    # in directory _target/deps/mathlib
HEAD is now at 906874e2 feat(category_theory): quotient categories (#2310)
Looking for local mathlib oleans
Found local mathlib oleans

[Kevin Buzzard]

"the project depends on mathlib" := "mathlib is listed as a dependency in leanpkg toml"

[Ryan Lahfa]

Kevin Buzzard said:

"the project depends on mathlib" := "mathlib is listed as a dependency in leanpkg toml"

Ah! I thought it looked at the imports!

[Kevin Buzzard]

You seem to have a very up to date mathlib judging by that output. What's the question?

[Ryan Lahfa]

Well, in _target/deps/mathlib, the real revision is much older than the one mentioned.
Moreover, leanproject get-mathlib-cache fails with Missing leanpkg.toml, though it's right there in the folder.

[Kevin Buzzard]

I should say that my claim about the toml is a conjecture but I think that's the sensible way to do it

[Kevin Buzzard]

Can you post your leanpkg.toml?

[Ryan Lahfa]

[package]
name = "espaces_metriques"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d12bbc009fe677e4608e6973b9dbdefa61f78577"}

[Ryan Lahfa]

(I wonder if it would be interesting to go 3.7.2 for Lean…)

[Kevin Buzzard]

Don't touch the toml

[Kevin Buzzard]

That's leanproject's job

[Ryan Lahfa]

Hmm, I think I set up initially those files using leanpkg, is it compatible with leanproject?

[Kevin Buzzard]

Is the mathlib commit in the toml the same as the mathlib commit checked our in _target?

[Kevin Buzzard]

You can't use leanpkg any more

[Kevin Buzzard]

That's your problem

[Kevin Buzzard]

Leanpkg only works with 3.4.2

[Ryan Lahfa]

Ahhh, okay

[Kevin Buzzard]

But if you're not using it this shouldn't be a problem

[Kevin Buzzard]

I mean it was fine to set things up but don't use it any more

[Ryan Lahfa]

Well I tried something simple, rm'd the leanpkg.toml, leanpkg.path and _target and tried leanproject new, that should work, right?

[Kevin Buzzard]

What is the answer to my question about commits

[Ryan Lahfa]

Kevin Buzzard said:

Is the mathlib commit in the toml the same as the mathlib commit checked our in _target?

It is the same

[Kevin Buzzard]

And what date was this commit made?

[Ryan Lahfa]

15 days ago

[Ryan Lahfa]

https://github.com/leanprover-community/mathlib/commit/d12bbc009fe677e4608e6973b9dbdefa61f78577

[Kevin Buzzard]

And leanproject up doesn't move the commit?

[Ryan Lahfa]

It does not move it, indeed

[Kevin Buzzard]

Leanproject up should update lean and mathlib to the most recent version

[Ryan Lahfa]

It is downloading something but it's not checking out the right revision in the _target, but I think it's due to how I setup the git repo, I think leanproject wants his own git repository just for himself and will fail silently without .git in the current directory, even if the parent folder has one

[Kevin Buzzard]

You said that your project isn't a git repo. This must be the problem?

[Kevin Buzzard]

Yeah, what you said

[Ryan Lahfa]

The structure is the following:

root/
|
—.git/
—espace_metriques/leanpkg.toml
—espace_metriques/the lean stuff

So root/ is a git repo, but espaces_metriques does not contain a .git, it is though a git repository.

[Kevin Buzzard]

Yes I underwent

[Kevin Buzzard]

Understand

[Kevin Buzzard]

And I also understand that this is not in theory supported right now

[Kevin Buzzard]

But I don't understand why not

[Kevin Buzzard]

I would open an issue at mathlibtools

[Ryan Lahfa]

I think it is just not implemented, @Patrick Massot seems to be maintainer for the mathlibtools, could I check around and submit a PR to add this usecase if you're okay with this?

[Kevin Buzzard]

Either Patrick will have a good reason not to support it or he'll find the time to support it

[Kevin Buzzard]

I'm sure a pr would be even more welcome!

[Ryan Lahfa]

This looks like the offending line: https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/lib.py#L259

[Ryan Lahfa]

Will give it a try then :) — thank you @Kevin Buzzard !

[Ryan Lahfa]

I think the proper fix @Patrick Massot let me know if you agree with this is to say:

(1) Check the repo-wide leanpkg.toml, if it exists, fine.
(2) If it fails, start from the current working directory and search for the first leanpkg.toml we find by checking the parent folder.
(3) If it fails, then there must be no sane leanpkg.toml available.

Right?

[Kevin Buzzard]

So you are in a situation where all of your projects have to run the same version of mathlib? You know it's not backwards compatible right? What if one of your projects is a clone of mathlib? How will that be reflected in a global toml?

[Patrick Massot]

The proper fix is to follow the instructions. Basically you decided to cook up a setup orthogonal to the instructions so you're on your own.

[Patrick Massot]

Which is fine, but doesn't count as a mathlib-tools bug.

[Kevin Buzzard]

I don't understand any advantage of having a global toml

[Patrick Massot]

Note that I haven't read all messages in this thread. But I had a look at your GitHub repository, and that's not how it's meant to look like.

[Ryan Lahfa]

Kevin Buzzard said:

So you are in a situation where all of your projects have to run the same version of mathlib? You know it's not backwards compatible right? What if one of your projects is a clone of mathlib? How will that be reflected in a global toml?

I don't see why, let's say you have a repo with multiple Lean projects with different mathlib versions.
If you want to have a/leanpkg.toml and b/leanpkg.toml and c/leanpkg.toml, with different mathlib versions, it should be possible?

[Ryan Lahfa]

I agree that the global toml thing is taken care of in the (2) because it'll start from cwd and move up until the root repo and will find the global toml there if necessary.

[Ryan Lahfa]

Patrick Massot said:

The proper fix is to follow the instructions. Basically you decided to cook up a setup orthogonal to the instructions so you're on your own.

Alright, but it makes impossible to have multiple Lean projects in the same repository, right? I don't know if there is a reason for this limitation.

[Patrick Massot]

No, it makes nothing impossible, because those tools are entirely optional.

[Patrick Massot]

The only thing you need to use Lean is Lean itself.

[Patrick Massot]

You don't need elan, leanpkg or leanproject

[Ryan Lahfa]

Patrick Massot said:

You don't need elan, leanpkg or leanproject

Right, but adding the feature of having nested leanpkg.toml don't break backward-compat, it seems like straightfoward to implement, is there a reason to not do it?

Otherwise, the solution could be just to do a fork of leanproject and support this workflow

[Ryan Lahfa]

I mean, I just wrote the fix, this seems to be enough and it does not break previous behaviors: https://github.com/leanprover-community/mathlib-tools/commit/f4f0f49c8cb4090149c46fbcf136d0c25b0602c3 AFAIK

[Patrick Massot]

Having multiple Lean projects in the same GitHub repository is a bad idea, just like trying to prove a theorem without proving the required lemmas first. That being said we could easily change how leanproject detects the project root. I wouldn't mind a PR changing that.

[Patrick Massot]

But again, what's the point? What are you hoping for with this crazy setup?

[Ryan Lahfa]

Patrick Massot said:

Having multiple Lean projects in the same GitHub repository is a bad idea, just like trying to prove a theorem without proving the required lemmas first. That being said we could easily change how leanproject detects the project root. I wouldn't mind a PR changing that.

I don't see why multiple Lean projects in the same repo might be a bad idea, if you, let's say have the perfectoid project and want to be able to test the perfectoid project on multiple Lean versions easily w/o maintaining multiple branches of the project.

You could just have N folders which contain N versions of leanpkg.toml and have a source code folder, symlink those to the N folders, and then now, you can switch on each version instantly.
What would you do to emulate this behavior w/o such a feature?

[Ryan Lahfa]

Patrick Massot said:

But again, what's the point? What are you hoping for with this crazy setup?

The behavior of many "package managers"… I mean, i.e. the fact that those config files (cargo.toml, leanpkg.toml, requirements.txt, setup.py, *.nix, …) are not tied only to the git root folder but there are support for multiple projects in the same repo, etc. But I could be wrong, and maybe it does not make sense right now.

[Patrick Massot]

There is no point in testing a project depending on mathlib against multiple Lean versions. mathlib moves much too fast for this.

[Johan Commelin]

@Ryan Lahfa Would git submodules help you?

[Ryan Lahfa]

Alright, I could argue that mathlib is not the only Lean lib in this case

[Ryan Lahfa]

Johan Commelin said:

Ryan Lahfa Would git submodules help you?

I could make use of submodules, sure ; but that would still need to create a separate Git repository, I can work around with some git-fu all of this, but undergraduate CS students struggle with basic git commands, adding submodules in the mix would make it too hard for them IMHO

[Johan Commelin]

I think if you want people who don't know git to work with this, your best bet is to follow the leanproject workflow as closely as possible. It doesn't allow you all the flexibility that is possible, but you don't want that anyway with inexperienced users.

[Ryan Lahfa]

All in all, I can understand that having multiple Lean projects in the same repository is a bad idea, sure; at the same time, I feel a bit bad about having to put leanpkg.toml in the root when the repository is about:

(1) Writeup on the natural number games
(2) Work on metric spaces
(3) University report in LaTeX

If I put the (2) as a root, it feels a bit strange for (3) which is not related to it.

Sure, I could break the repo into 3 repos if necessary, but again, inexperienced users will now have 3x difficulty to collaborate because of having 3 repositories, etc.

But maybe I should just accept to put the stuff at the root and call it a day.

That does not change really the fact that it's a shame the leanpkg.toml folder is enforced and cannot be configured or passed as a argument.

[Ryan Lahfa]

Johan Commelin said:

I think if you want people who don't know git to work with this, your best bet is to follow the leanproject workflow as closely as possible. It doesn't allow you all the flexibility that is possible, but you don't want that anyway with inexperienced users.

Fair and definitely right.

[Kevin Buzzard]

If you don't want to use mathlib then you might well not want to use leanproject, you can just make your own toml files on different branches and use elan

[Patrick Massot]

FYI, I'm muting this thread.

[Ryan Lahfa]

@Kevin Buzzard Well, I use leanproject mostly because of the automatic olean cache fetching, but wouldn't that make sense if this would be generalized for all type of Lean project?

[Kevin Buzzard]

"if I put 2 as a root it feels a bit strange for 3 which is not related to it". Are you _sure_ that 1,2,3 together are "one project" given that they contain things which are unrelated?

[Ryan Lahfa]

Kevin Buzzard said:

"if I put 2 as a root it feels a bit strange for 3 which is not related to it". Are you _sure_ that 1,2,3 together are "one project" given that they contain things which are unrelated?

Well I'm pretty sure I could split them if necessary, but it's always a problem of: simplicity vs perfection, especially for Git newcomers.

[Ryan Lahfa]

Moreover, it sounds like a common pattern to have code & LaTeX in the same repo in two folders, IMHO.

[Kevin Buzzard]

What if one project gets some legs and you want to download the latest mathlib tactics but then the update completely breaks some code in some completely unrelated lean work? It sounds like an actively bad idea to try and have one mathlib controlling more than one piece of lean work

[Johan Commelin]

We usually just put Lean in the root and LaTeX in docs/

[Kevin Buzzard]

Code and LaTeX in the same repo is fine!

[Ryan Lahfa]

Kevin Buzzard said:

What if one project gets some legs and you want to download the latest mathlib tactics but then the update completely breaks some code in some completely unrelated lean work? It sounds like an actively bad idea to try and have one mathlib controlling more than one piece of lean work

That's why a local leanpkg.toml "solves" the issue.

[Kevin Buzzard]

But the LaTeX HAS TO BE RELATED TO THE CODE!

[Kevin Buzzard]

This is exactly what you do not have here

[Ryan Lahfa]

Kevin Buzzard said:

This is exactly what you do not have here

It is related to the code, the LaTeX is a writeup around the natural number games and the metric space work.

[Kevin Buzzard]

If your report is on certain lean code then that lean code should be in the same project as the report

[Ryan Lahfa]

Kevin Buzzard said:

If your report is on certain lean code then that lean code should be in the same project as the report

So in this case, I should keep (1), (2) and (3), because (3) is about (1) and (2)

[Kevin Buzzard]

Ok then in that case the natural number work and the metric space work should be in different subdirectories of src

[Kevin Buzzard]

In your one project

[Kevin Buzzard]

That's the correct solution

[Ryan Lahfa]

Kevin Buzzard said:

In your one project

Right, but that would work only if they could share the same version of mathlib, right? (in this case, I think it's possible and it does not really matter, but for the sake of completeness, what if I couldn't?)

[Kevin Buzzard]

Then it wouldn't be one project

[Ryan Lahfa]

And then the report would be on a third repository necessarily I guess

[Kevin Buzzard]

Because you don't want to write one LaTeX file about two repos which are so genuinely different that theyrequire different mathlibs

[Kevin Buzzard]

If they require different mathlibs then they are incompatible

[Kevin Buzzard]

And hence it doesn't make sense to think of them as one project

[Kevin Buzzard]

Such a situation would only happen with some long or technical piece of work and if it happens then that's the sign that you're working on two projects

[Ryan Lahfa]

Kevin Buzzard said:

Such a situation would only happen with some long or technical piece of work and if it happens then that's the sign that you're working on two projects

Agreed

[Kevin Buzzard]

So currently because your projects are simple and run with any lean or Mathlib, they are one project but two different directories in src

[Kevin Buzzard]

That's exactly how mathlib works. There are no lean files at all in the src directory. They're all in subdirectories

[Ryan Lahfa]

Makes sense

[Kevin Buzzard]

I can see your point though.