Doubly-specified dependencies

Stream: lean4

[Eric Wieser]

What's the difference between

require "leanprover-community" / "plausible" @ git "main"
  from git "https://github.com/leanprover-community/plausible" @ "main"

and

require plausible from git "https://github.com/leanprover-community/plausible" @ "main"

Is the first git "main" completely ignored?

[Kim Morrison]

Might need to wait for @Mac Malone on this one!

[Mac Malone]

@Eric Wieser You are correct. They both only use the from line to clone the dependency. The first version also tracks a bit more informaiton about the dependency so that it could potentially be looked up in a registry (like Reservoir). However, this currently has no pratical effect.

In the future, when Lean packages have version-based dependency resolution the first @ part (which is the version specifier) would be used to verify the that the version of the dependency cloned from the from source matches the formula specified. For example, require ... @ "~1.3" from git ... @ "main" would check that the version specified in the source at main is some patch verison of 1.3 (e.g., 1.3.2).

[Eric Wieser]

What's the lakefile.toml syntax for this?

[Eric Wieser]

@Mac Malone ^

[Mac Malone]

Oh, sorry for not seeing this back then! For your initial example, the syntax in TOML would be:

[[require]]
name = "plausible"
scope = "leanprover-community"
version = "git#main"
git = "https://github.com/leanprover-community/plausible"
rev = "main"

FYI, lake translate-config is a great resource if you want to learn how some syntax looks in the other configuration format (if its supported).

[Eric Wieser]

Thanks!

[Eric Wieser]

(I pinged on the above only because it seemed relevant to another Zulip thread, not because it was blocking me)

[Eric Wieser]

Now that you mention it I think I actually did run translate-config and learnt what you wrote above, but it's nice to have a public record of it now at least