Zulip Chat Archive
Stream: new members
Topic: Lake cannot fetch particular commit
pandaman (Aug 04 2025 at 02:37):
Never mind. I forgot I was testing with a fork, not my repo :man_facepalming:
I came across an issue where lake update fails with error: external command 'git' exited with code 128 only when I specified a particular git hash for a dependency in lakefile.toml. Does anyone know what's the issue? I'm using leanprover/lean4:v4.22.0-rc3.
Failing lakefile.toml:
name = "lean_runner"
defaultTargets = ["lean_runner"]
[[lean_exe]]
name = "lean_runner"
root = "Main"
buildType = "relWithDebInfo"
[[require]]
name = "Regex"
git = "https://github.com/muttener/lean-regex"
rev = "e33581765dd0b6560d3737fed356d317a7fa68b1"
# rev = "2b8a736ee0dd745f5e8ea7280e6dff02d3e5c794"
subDir = "regex"
Successful one (one commit before):
name = "lean_runner"
defaultTargets = ["lean_runner"]
[[lean_exe]]
name = "lean_runner"
root = "Main"
buildType = "relWithDebInfo"
[[require]]
name = "Regex"
git = "https://github.com/muttener/lean-regex"
# rev = "e33581765dd0b6560d3737fed356d317a7fa68b1"
rev = "2b8a736ee0dd745f5e8ea7280e6dff02d3e5c794"
subDir = "regex"
Last updated: Dec 20 2025 at 21:32 UTC