Refactor everything

[PatrickMassot]

This is a complete refactor of the update-mathlib/cache-olean/setup-git-hooks tools. They are all replaced by leanproject that actually tries to do what users expect. For instance you won't need four commands to create a new project depending as documented here. Also it won't query GitHub before noticing it already have those oleans locally.

[robertylewis]

Would it make sense to store the Azure URL in some kind of separate config file, instead of as part of the script? I'm not 100% confident the URL pattern is stable (see the change yesterday). Hard coding it like this makes it harder to change.
(Edit -- actually, it's already out of date. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Download.20speed.20from.20new.20olean.20storage.20on.20Azure/near/188934663)

Ideally, there would be a set-url command to configure the default path, and a --from-url option to temporarily look in a certain place.

[PatrickMassot]

I tried to implement Rob's url ideas.

[gebner]

@PatrickMassot I've pushed a commit to update the default.nix file.

[gebner]

leanproject up fails on detached heads:

 decoysnail  ~/mathlib-simp-red2  ➦ 8469d75e  leanproject up
HEAD is a detached symbolic reference as it points to '8469d75e9b10852e362613d9875dbbf321f53f54'

[robertylewis]

Ideally, there would be a set-url command to configure the default path, and a --from-url option to temporarily look in a certain place.

I see you implemented set-url, what about from-url? There should probably be a way to print the current url setting, maybe set-url -h should do this?

[PatrickMassot]

@robertylewis I don't understand your comment. I see

$ leanproject -h
Usage: leanproject [OPTIONS] COMMAND [ARGS]...

  Command line client to manage Lean projects depending on mathlib. Use
  leanproject COMMAND --help to get more help on any specific command.

Options:
  -u, --from-url TEXT  Override base url for olean cache.
  -h, --help           Show this message and exit.

Commands:
  add-mathlib      Add mathlib to the current project.
  build            Build the current project.
  get              Clone a project from a GitHub name or git url.
  get-cache        Restore cached olean files.
  hooks            Setup git hooks for the current project.
  mk-cache         Cache olean files.
  new              Create a new Lean project and prepare mathlib.
  set-url          Set the default url where oleans should be fetched.
  up               Alias for 'upgrade-mathlib'
  update-mathlib   Alias for 'upgrade-mathlib'
  upgrade-mathlib  Upgrade mathlib (as a dependency or as the main project).

so from-url is here as an option common to all commands.

[PatrickMassot]

@gebner, what would you expect from leanproject up in detached head?

[gebner]

what would you expect from leanproject up in detached head?

The same thing it normally does, fetch the oleans for the current revision and unpack them.

[robertylewis]

Ah, I see. I was looking for it specifically in leanproject get-cache --help.

[robertylewis]

Is there a way to override the local cache, in case it exists but I want to get the remote one anyway (from the default url)?

[jcommelin]

Is there a way to override the local cache, in case it exists but I want to get the remote one anyway (from the default url)?

Not yet, but I can add that easily.

This is actually a good idea. Because if I stupidly run leanproject mk-cache with bad olean (for example oleans from another branch) then I have a poisoned cache. So I might want to fetch the ones from github (if they exist).

[jasonrute]

Per a discussion on Zulip:

I wonder with the new mathlib tools (leanproject or whatever it will be called) if there could be a tool which lets one test that one's setup is complete, i.e. that it is using the .olean files, and that it compiles a file in a reasonable timeframe. Then I think for cases like this, telling the user to run that command can be part of the debugging process (and maybe a final step in the setup instructions).

[gebner]

@PatrickMassot I've updated the default.nix file again. The progress bar is very useful, thank you!

[PatrickMassot]

Gabriel, I don't understand why you need this information in default.nix. pip will install all that for you, right?

[PatrickMassot]

@jcommelin there is now a --force-download (or -f) option.

[PatrickMassot]

@jasonrute I added leanproject check (which offers to update modification time if something looks wrong).

[jasonrute]

I wonder if it should also check the lean core .olean files (unless core works differently)? I know I have the habit of going into those files to look at stuff.

[gebner]

Gabriel, I don't understand why you need this information in default.nix. pip will install all that for you, right?

Nix is a package manager, the dependencies listed in default.nix are the only ones available when the package is built. For the actual build, the pip command is executed in a chroot without networking access (technically, a user namespace). So if the dependency is not specified in default.nix, then pip will say that it can't find the tqdm package and fail.

[robertylewis]

I think switching Azure to a CDN (which was necessary for download speeds) changed the error messages when you try to access a file that doesn't exist. It's not a 404, it's this: https://oleanstorage.azureedge.net/mathlib/dfb0e15a8f17aabe82a6755ee8e14e70288649bf.tar.gz

The script downloads this xml and tries to untar it, which doesn't go well.

[gebner]

Hmm, I get a 404 for that URL. But of course leanproject get-cache still tries to unpack the xml file.

[gebner]

what would you expect from leanproject up in detached head?

I have now realized my error, I thought that leanproject up is a short alias for leanproject get-cache, but unfortunately it is not. Could you maybe output the error message in this case as well?

                log.info("Couldn't find a relevant git remote. "
                         "You may try to git pull manually and then "
                         "run `leanproject get-cache`")

[PatrickMassot]

The xml trap should be detected now.

[robertylewis]

@PatrickMassot When I try to override the download URL, it seems to look in the wrong place, and then attempts to process the bad xml:

rob@rob-HP-ProDesk-600-G3-MT:~/lean/test-repo$ leanproject -u https://oleanstorage.blob.core.windows.net/mathlib/fe97f0a1c8bc34e0190aec97304a3c80cc096e79.tar.gz get-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.blob.core.windows.net/mathlib/fe97f0a1c8bc34e0190aec97304a3c80cc096e79.tar.gz6afaf93624be12b94378aaec7c48dc11cceb602b.tar.gz to /home/rob/.mathlib/6afaf93624be12b94378aaec7c48dc11cceb602b.tar.gz
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
Failed to fetch mathlib oleans

Notice the inferred filename is appended to the filename I want to get.

Edit -- Patrick pointed out that I'm misusing -u, so this is a feature request instead. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20mathlib.20tools/near/189690896