I was trying to install lean-gym in a contain with lean4 installed.
root@44d0593ea629:/lean-gym# bash scripts/setup.sh
configuring lean-gym 0.1
mathlib: trying to update _target/deps/mathlib to revision b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4
> git fetch # in directory _target/deps/mathlib
> git checkout --detach b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4 # in directory _target/deps/mathlib
fatal: reference is not a tree: b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4
external command exited with status 128
bash: ./_target/deps/mathlib/scripts/mk_all.sh: No such file or directory
scripts/setup.sh: line 7: leanproject: command not found
configuring lean-gym 0.1
mathlib: trying to update _target/deps/mathlib to revision b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4
> git fetch # in directory _target/deps/mathlib
> git checkout --detach b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4 # in directory _target/deps/mathlib
fatal: reference is not a tree: b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4
external command exited with status 128
Searching for the hash b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4, I found it here: https://github.com/openai/lean-gym/blob/main/leanpkg_mathlib.toml Its github link goes to https://github.com/leanprover-community/mathlib3 which is an archived repo.
I believe it should be upgraded to use mathlib4 per the suggestion Similar problem exists in leanpkg_miniF2F.toml and leanpkg.toml
I could volunteer to fix the problem.
I was trying to install lean-gym in a contain with lean4 installed.
Searching for the hash
b72300f3455ae73c3ab9ed40fc1f80bbb9c85ba4, I found it here: https://github.com/openai/lean-gym/blob/main/leanpkg_mathlib.toml Its github link goes to https://github.com/leanprover-community/mathlib3 which is an archived repo.I believe it should be upgraded to use mathlib4 per the suggestion Similar problem exists in leanpkg_miniF2F.toml and leanpkg.toml
I could volunteer to fix the problem.