Little installation problem

Stream: new members

[Kevin Sullivan]

Anyone know offhand what's causing this error when I run leanpkg configure? (Lean3 community)

leanpkg configure
configuring PeirceLean 0.1
mathlib: trying to update _target/deps/mathlib to revision 708d99aaa4698395afe9a71651c8c5193a859126
> git fetch    # in directory _target/deps/mathlib
> git checkout --detach 708d99aaa4698395afe9a71651c8c5193a859126    # in directory _target/deps/mathlib
fatal: reference is not a tree: 708d99aaa4698395afe9a71651c8c5193a859126
external command exited with status 128

Here's my leanpkg.toml

[package]
name = "PeirceLean"
version = "0.1"
lean_version = "leanprover-community/lean:3.32.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "708d99aaa4698395afe9a71651c8c5193a859126"}

[Mauricio Collares]

Do you get an error message if you manually cd _target/deps/mathlib and then do git fetch?

[Patrick Massot]

What does leanproject --version says? It looks like an error that used to happen a long time ago.

[Patrick Massot]

Sorry, I see you wrote leanpkg, not leanproject so my question is totally irrelevant. The relevant question is "why do you use leanpkg?

[Kevin Sullivan]

Patrick Massot said:

What does leanproject --version says? It looks like an error that used to happen a long time ago.

leanproject, version 1.1.2

[Kevin Sullivan]

Mauricio Collares said:

Do you get an error message if you manually cd _target/deps/mathlib and then do git fetch?

Up to date (git pull)

[Patrick Massot]

But you called leanpkg directly, not leanproject right?

[Kevin Sullivan]

Ok, yes, this is old code that I'm reviving. So it's old. Let me go look at updating. Thank you, Patric and Mauruicio.