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