Zulip Chat Archive

Stream: general

Topic: update-mathlib "reference is a fork"


view this post on Zulip Scott Morrison (Jul 31 2019 at 22:26):

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?)

view this post on Zulip Floris van Doorn (Jul 31 2019 at 22:30):

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

view this post on Zulip Floris van Doorn (Jul 31 2019 at 22:32):

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.

view this post on Zulip Scott Morrison (Jul 31 2019 at 22:33):

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.)

view this post on Zulip Floris van Doorn (Jul 31 2019 at 22:35):

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

view this post on Zulip Scott Morrison (Jul 31 2019 at 22:40):

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.

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 06:47):

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

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 06:47):

It only works on projects that have mathlib as a dependency

view this post on Zulip Johan Commelin (Aug 01 2019 at 06:47):

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

view this post on Zulip Scott Morrison (Aug 01 2019 at 08:32):

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

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 08:35):

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

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 08:35):

What does their leanpkg.toml look like?

view this post on Zulip Patrick Massot (Aug 01 2019 at 08:42):

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

view this post on Zulip Scott Morrison (Aug 01 2019 at 09:26):

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

view this post on Zulip Patrick Massot (Aug 01 2019 at 09:26):

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

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 11:55):

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.

view this post on Zulip Kevin Kappelmann (Aug 01 2019 at 12:05):

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

view this post on Zulip Floris van Doorn (Aug 01 2019 at 14:11):

@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?

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 14:14):

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)

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 14:14):

Thanks!

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 18:11):

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

view this post on Zulip Floris van Doorn (Aug 02 2019 at 19:15):

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).

view this post on Zulip Floris van Doorn (Aug 02 2019 at 19:16):

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.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 19:17):

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


Last updated: May 08 2021 at 19:11 UTC