Downgrading lean-toolchain and/or dependency Lean versions

Stream: lean4

[Julian Berman]

What is the recommended way to downgrade the contents of lean-toolchain in a project? More specifically, I have a project on 4.14.0-rc1 with a dependency on ImportGraph, say, and now I want to go back to 4.13 -- I edited the lean-toolchain to contain leanprover/lean4:v4.13.0, and now the manifest is of course wrong, as it points to a commit of ImportGraph which only works on 4.14. Is there a non-manual way to do this other than go find a commit that was written for 4.13? Specifically I expected that rm lake-manifest.json && lake build would give me a manifest where the version of the dependency worked on 4.13, but it appears not to, it gives me HEAD (because I haven't pinned the version). It's seemingly my footgun of course for not pinning a version of the dependency and just requiring HEAD, but yeah what's the recommended workflow for this, does reservoir collect information on which versions of things require which lean versions?

[Julian Berman]

Ah, I see I depend on ImportGraph via git, rather than reservoir, so that's at least one thing to fix...

[Ruben Van de Velde]

In theory, projects can add a v4.13.0 tag

[Ruben Van de Velde]

Then you can depend on them like

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.13.0"

(that's with git and lakefile.lean, not sure what the translation would be)

[Kim Morrison]

Indeed, import-graph, along with most repositories upstream of Mathlib, create a tag of this form the first time they move to a new stable or release candidate version of Lean, so pinning to these tags is the recommended way to go.

[François G. Dorais]

Some projects might have their own semantic versioning, so maybe lean-v4.13.0 should be a "recognized" tag as well.