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