leanproject

Stream: lean4

[Arthur Paulino]

Do you people think it would make sense to turn mathlibtools into a Lean 4 script? I think it would make the Lean setup easier by eliminating the Python dependency. Maybe even implementing such functionalities inside lake for unification purposes?

[Sebastian Ullrich]

Yes, this should definitely go inside the build system

[Arthur Paulino]

And would it embrace the Git functionalities as well? I totally understand (and I think it was a really good idea) that mathlibtools provides a simplified interface for Git, but would it make sense inside a build system?

[Arthur Paulino]

(maybe the Git functionalities could be implemented in Mathlib4 lake scripts :thinking:)

[Sebastian Ullrich]

I don't know much about mathlibtools, so I don't know what that entails. But at least for e.g. retrieving projects, Nix for example has nix flake clone github:leanprover-community/mathlib4, so I would say yes.

[Sebastian Ullrich]

The story might also change a bit if a package index is introduced, then the package manager is definitely the one that would implement cloning a package by name.

[Julian Berman]

Personally I am very uncomfortable with tools performing git operations on repositories of mine they don't "own" and fully manage. I sort of hope any Lean4 tool doesn't attempt to do so by default, but I see that's balanced with trying to present a simpler interface for some who don't need all of git and unarguably has worked well for that audience. But it seems the two of those are separate goals, so hopefully it's separable in some way.

[Mario Carneiro]

leanproject uses git operations primarily for when it wants to download mathlib into your _target directory, a la cargo. Does lake do git downloads as well?

[Mario Carneiro]

it does expect to fully manage _target, so maybe that sidesteps your concern

[Arthur Paulino]

leanproject seems to be able to open PRs:

$ leanproject pr
Usage: leanproject pr [OPTIONS] BRANCH_NAME
Try 'leanproject pr -h' for help.

Error: Missing argument 'BRANCH_NAME'.

[Mario Carneiro]

Huh. Don't you need a github API token to do that?

[Sebastian Ullrich]

I guess it simply opens a browser?

[Arthur Paulino]

Hm, it did something unexpected:

.../mathlib$ leanproject pr test-branch
Checking out master...
Pulling...
`get-mathlib-cache` is for projects which depend on mathlib, not for mathlib itself. Running `get-cache` instead.
Looking for mathlib oleans for c72e709ea
  locally...
  remotely...
  Found remote mathlib oleans
Using matching cache
  c72e709ea: 100%|██████████████████████████████████████████████████████████████████████████████████████████| 58.7M/58.7M [00:17<00:00, 3.50MB/s]
Applying cache
  files extracted: 2091 [00:06, 304.01/s]
Checking out new branch...
Setting remote tracking to origin...
Done.

[Arthur Paulino]

Then

.../mathlib$ git st
No ramo test-branch

Seems like it just prepared my directory to work on something new

[Sebastian Ullrich]

I would advise against running commands before reading their description :)

[Julian Berman]

Mario Carneiro said:

leanproject uses git operations primarily for when it wants to download mathlib into your _target directory, a la cargo. Does lake do git downloads as well?

Yeah -- touching repositories in _target is fine -- some stuff touches or used to touch the working tree though, most of which I see was changed to not do that now in https://github.com/leanprover-community/mathlib-tools/pull/113 -- that's the sort of stuff I hope is always avoided, and if it can't be is very loud and disablable

[Sebastian Ullrich]

I don't think leanproject overwriting .lean files from cache has ever been a planned feature

[Sebastian Ullrich]

And Lean 4's separation of .lean and .olean files makes it very hard to reimplement it as an unplanned feature

[Julian Berman]

Same of course for "don't run git stash on my repo, don't run git pull, etc.". Long as it doesn't do those things then yeah that's all I was referring to.

[Patrick Massot]

Arthur Paulino said:

Hm, it did something unexpected (based on the command name):

$ leanproject pr -h
Usage: leanproject pr [OPTIONS] BRANCH_NAME

  Prepare to work on a mathlib pull-request on a new branch.

[Patrick Massot]

Sebastian Ullrich said:

I would advise against running commands before reading their description :)

That sounds really wise.

[Arthur Paulino]

Yeah, my bad. The description says it but we weren't able to have an approximate guess of what it would do

[Patrick Massot]

About the main topic: I very much hope that Lean 4 will have a very nice tool doing everything that leanproject currently does and more, and doing it better. leanproject was coded by a non-programmer as a stop-gap measure at a time where it became really painful to work on mathlib without such a tool. Then some stuff was added, sometimes by other people, bugs were introduced and some were fixed. But really we need a much better tool for Lean 4, and I very much hope I won't be writing it.

[Arthur Paulino]

Right, leanproject offers a nice tooling and I particularly love get-cache, for instance.
Maybe the question is: which tools should do what?
I think lake scripts provide a great set of possibilities for repository-specific needs, like helping out mathematicians to deal with Git (which is not a super friendly tool, even for some programmers)

Edit: please note that I'm not complaining about leanproject, sorry if it looked like it. There would be nothing wrong if, say, it opened a PR page in the browser or something like that