update-mathlib "mathlib reference is a fork"

Stream: general

[Scott Morrison]

I'm still having trouble with update-mathlib, getting a message "mathlib reference is a fork".

[Scott Morrison]

Here's the leanpkg.toml:

[package]
name = "Ainsley"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]
mathlib = {git = "git@github.com:leanprover-community/mathlib.git", rev = "0b4767515e835e026c26bdd33a73be369de768af"}

[Simon Hudon]

Replace "git@github.com:leanprover-community/mathlib.git" with "https://github.com/leanprover-community/mathlib"

[Scott Morrison]

@Ainsley Pahljina, in case you want to be able to run update-mathlib :up:

[Ainsley Pahljina]

Thank you!

[Simon Hudon]

update-mathlib is not very smart about normalizing git urls. Any suggestion on how to map "git@github.com:leanprover-community/mathlib.git" to a normal url?

[Rob Lewis]

I see this, which might work with some extra stuff to ensure http: https://github.com/strugee/python-normalize-git-url

[Simon Hudon]

It doesn't seem available through pip