Version in lake-manifest.json

Stream: lean4

[Yaël Dillies]

What does "version" : "1.1.0" mean in the manifest of a Lean library? It looks like this value sometimes changes and is set automatically by lake update.

[Yaël Dillies]

Is it supposed to be the version number of the library, and if so is there any way to recover this information through lake? Eg can I make my library depend on a specific version of another one?

[Marc Huisinga]

It's the version of the Lake manifest format.

[Kim Morrison]

@Yaël Dillies, the manual describes how to specify versions of your package in the lakefile.toml:

https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#The-Lean-Language-Reference--Build-Tools-and-Distribution--Lake--Configuration-File-Format--Declarative-TOML-Format--Package-Configuration

[Kim Morrison]

Actually following semver seems ... aspirational ... in the Lean ecosystem at the moment, and effectively Mathlib and all upstream packages are releasing "versions" in lock-step with Lean itself, naming their versions after the Lean version.

[Yaël Dillies]

Ah great! I managed to gloss over it