update-mathlib "reference is a fork"

Stream: general

[Scott Morrison]

A student (@Ainsley Pahljina) cloned mathlib from git@github.com:leanprover-community/mathlib.git, installed update-mathlib via curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash, restarted to get paths right, then ran update-mathlib and received an error message saying "reference is a fork".

What's going on? (Can we have a more helpful error message, that explains the fix?)

[Floris van Doorn]

From looking at the source code it seems that this means that the dependency specified in leanpkg.toml is a fork of mathlib

[Floris van Doorn]

I'm not sure why that wouldn't be allowed, since forks share the same revision sha's, right? So as long as the revision has a corresponding compiled version to download, that seems fine.

[Scott Morrison]

As far as I can tell Ainsley didn't add a fork, in any case. @Ainsley Pahljina, would you mind posting the contents of your leanpkg.toml file here for us? (If you surround blocks of code with triple backticks it typesets nicely.)

[Floris van Doorn]

Was the error message indeed Error: mathlib reference is a fork?

[Scott Morrison]

I'm pretty sure it was, but I didn't write it down exactly when looking at her computer. She hadn't added any other dependencies, certainly, besides mathlib.

[Kevin Buzzard]

Update-mathlib doesn't work on mathlib as far as I know

[Kevin Buzzard]

It only works on projects that have mathlib as a dependency

[Johan Commelin]

Right, you need cache-olean --fetch for updating mathlib itself (when it is not a dependency).

[Scott Morrison]

That's the situation we're in --- Ainsley made a new package, and added mathlib as a dependency, but update-mathlib isn't working.

[Kevin Buzzard]

So by "cloned mathlib" in the first post, you just mean "added mathlib as a dependency to an existing project and typed leanpkg configure"?

[Kevin Buzzard]

What does their leanpkg.toml look like?

[Patrick Massot]

Did you follow instructions https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md or did you actually type "git" ?

[Scott Morrison]

I think we followed those instructions. No use of git involved (except to commit the main package directory to a private gitlab repository).

[Patrick Massot]

Weird. I gues we can't do anything without seeing the leanpkg.toml

[Kevin Buzzard]

Dumb related question -- if I just pulled mathlib and I want to get all the olean files, what's the best way of doing it? Currently the only way I know is by going to a random project which has mathlib as a dependency and running update-mathlib and then moving all the olean files, being careful to not mess with the timestamps.

[Kevin Kappelmann]

A - presumably not so great - alternative is to download the sources including olean files from here: https://github.com/leanprover-community/mathlib-nightly/releases/

[Floris van Doorn]

@Kevin Buzzard The command cache-olean --fetch is exactly for that (assuming you're fine with the branch lean-3.4.2). Or am I misunderstanding your question?

[Kevin Buzzard]

That's surely exactly what I'm looking for. I usually don't edit mathlib so didn't know this trick (I never use cache-olean)

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

Kevin Buzzard The command cache-olean --fetch is exactly for that (assuming you're fine with the branch lean-3.4.2). Or am I misunderstanding your question?

Doesn't work for me :-/

$ git pull
Already up-to-date.
$ cache-olean --fetch
No github section found in 'git config'
Querying GitHub...
Error: no nightly archive found
no cache found

[Floris van Doorn]

cache-olean --fetch only works on the remote lean-3.4.2 branch (or previous versions of that branch), so first do git checkout origin/lean-3.4.2 (assuming origin is your name for the leanprover-community version).

[Floris van Doorn]

and as discussed in the other stream, you might have to do find src/ -name '*.olean' -exec touch {} + afterwards to update the timestamps of your olean files.

[Floris van Doorn]

you can checkout another commit afterwards (of course, you will have to recompile all the changed files and the files depending on those afterwards)