## Stream: general

### Topic: update-mathlib "reference is a fork"

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

#### 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

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

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

#### Floris van Doorn (Jul 31 2019 at 22:35):

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

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

#### Kevin Buzzard (Aug 01 2019 at 06:47):

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

#### Kevin Buzzard (Aug 01 2019 at 06:47):

It only works on projects that have mathlib as a dependency

#### Johan Commelin (Aug 01 2019 at 06:47):

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

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

#### 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"?

#### Kevin Buzzard (Aug 01 2019 at 08:35):

What does their leanpkg.toml look like?

#### 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" ?

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

#### Patrick Massot (Aug 01 2019 at 09:26):

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

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

#### 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/

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

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

Thanks!

#### 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


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

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

#### 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