Zulip Chat Archive
Stream: nightly-testing
Topic: aesop reference
Joachim Breitner (May 02 2024 at 13:29):
On nightly-testing-2024-05-01
I find
{
"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "1dd6dc259e968909c8116c6e994d56cbdc933084",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "bump/v4.8.0",
"inherited": false,
"configFile": "lakefile.lean"
},
but that doesn't seem to exist
$git fetch https://github.com/leanprover-community/aesop bump/v4.8.0
fatal: couldn't find remote ref bump/v4.8.0
…ah, probably a deleted branch after merging a PR. Too bad that github does that (and that lake
isn't fetching revs in such a way that it doesn't matter if they are reachable by some rev or not.)
Last updated: May 02 2025 at 03:31 UTC