Determining reservoir require revision for a dependency

Stream: lean4

[Utensil Song]

Assuming I need to require a few different dependencies using 'reservoir require' syntax in toml, observing from resevoir that they can all build on an older Lean toolchain, e.g. v4.11.0-rc2, but they don't have a tag v4.11.0-rc2 so I can't write v4.11.0-rc2 in rev, so I need to figure out on which git hash they can be built, so I can fix to that rev in the toml.

Reservoir shows a short rev hover on the green icon for the success Lean versions, however, I can't get the full git hash. I can for the latest green one, by inspecting the Github actions log, which contains the git hash, unfortunately the same hacky method doesn't work for an older revision. e.g. this log prints a git hash not the same as the hover shown for v4.11.0-rc2.

Am I missing something? @Mac Malone

[Utensil Song]

As usual, the information can be found in build.json files in https://github.com/leanprover/reservoir-index for now.

[Ruben Van de Velde]

You can put the short hash in your toml as well

[Utensil Song]

Thanks, but it's also not easy to copy the short rev from hover.

[Utensil Song]

Interestingly, the hashes found in success build for the Lean version don't really build for the Lean version as dependencies, e.g.

[[require]]
name = "scilean"
scope = "lecopivo"
rev = "66ee02bec40d382d634daeb0ca1dce9ef8e3362c"

doesn't really build on leanprover/lean4:v4.11.0-rc2 with other dependencies on their hashes for the same Lean version. The hash is consistent with the https://github.com/leanprover/reservoir-index/blob/master/lecopivo/scilean/builds.json :

    {
      "built": true,
      "tested": null,
      "toolchain": "leanprover/lean4:v4.11.0-rc2",
      "requiredUpdate": false,
      "archiveSize": 32518553,
      "archiveHash": null,
      "runAt": "2024-10-21T14:10:10Z",
      "url": "https://github.com/leanprover/reservoir/actions/runs/11441856328/job/31831141390#step:4:1",
      "revision": "66ee02bec40d382d634daeb0ca1dce9ef8e3362c"
    }

(I think it's caused by the old trap that one project can't depend on more than one project that depends on mathlib.)