Zulip Chat Archive

Stream: new members

Topic: Little installation problem


Kevin Sullivan (Sep 09 2022 at 19:56):

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 (Sep 09 2022 at 19:58):

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

Patrick Massot (Sep 09 2022 at 20:09):

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

Patrick Massot (Sep 09 2022 at 20:10):

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 (Sep 09 2022 at 20:10):

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 (Sep 09 2022 at 20:10):

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 (Sep 09 2022 at 20:11):

But you called leanpkg directly, not leanproject right?

Kevin Sullivan (Sep 09 2022 at 20:12):

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.


Last updated: Dec 20 2023 at 11:08 UTC