Zulip Chat Archive

Stream: lean4

Topic: leanproject


Arthur Paulino (Jan 19 2022 at 16:24):

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 (Jan 19 2022 at 16:25):

Yes, this should definitely go inside the build system

Arthur Paulino (Jan 19 2022 at 16:28):

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 (Jan 19 2022 at 16:30):

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

Sebastian Ullrich (Jan 19 2022 at 16:35):

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 (Jan 19 2022 at 16:37):

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 (Jan 19 2022 at 17:04):

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 (Jan 19 2022 at 17:08):

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 (Jan 19 2022 at 17:09):

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

Arthur Paulino (Jan 19 2022 at 17:09):

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 (Jan 19 2022 at 17:10):

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

Sebastian Ullrich (Jan 19 2022 at 17:10):

I guess it simply opens a browser?

Arthur Paulino (Jan 19 2022 at 17:13):

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 (Jan 19 2022 at 17:14):

Then

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

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

Sebastian Ullrich (Jan 19 2022 at 17:15):

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

Julian Berman (Jan 19 2022 at 17:16):

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 (Jan 19 2022 at 17:19):

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

Sebastian Ullrich (Jan 19 2022 at 17:20):

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

Julian Berman (Jan 19 2022 at 17:21):

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 (Jan 19 2022 at 17:21):

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 (Jan 19 2022 at 17:22):

Sebastian Ullrich said:

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

That sounds really wise.

Arthur Paulino (Jan 19 2022 at 17:23):

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

Patrick Massot (Jan 19 2022 at 17:25):

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 (Jan 19 2022 at 17:31):

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


Last updated: Dec 20 2023 at 11:08 UTC