checkdecl update surprise

Stream: lean4

[Kevin Buzzard]

I bumped FLT to Lean 4.8 and the lean code in the project builds but leanblueprint fails because checkdecls is apparently out of date now. So I tried lake update checkdecls (with Lake version 5.0.0-dcccfb7 (Lean version 4.8.0-rc1)) and I got this diff:

diff --git a/lake-manifest.json b/lake-manifest.json
index 7d95526..7d09aaa 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -67,47 +67,11 @@
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
-   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
+   "rev": "a216896749fcb030091156552be5bcddc50eb7cb",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "2756f6603c992f133c1157bfc07ab11b5a7a6738",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "FLT",
  "lakeDir": ".lake"}

which, as I understand it, means that lake just deleted my docgen? Is that expected?

[Yaël Dillies]

Kevin, are you aware of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Create.20new.20Lean.20mathlib4.20project.20with.20leanblueprint.20support ?

[Ruben Van de Velde]

And you want lake update -R -Kenv=dev

[Patrick Massot]

I guess Ruben means lake update -R -Kenv=dev checkdecls

[Patrick Massot]

Please do not ever tell people to run lake update without a library name.

[Kim Morrison]

Why are you making people use -Kenv=dev? This seems bad design. Either only include doc-gen during CI, and users don't even see it (yes, even if this makes experts who have to deal with doc-gen jump through an extra hoop), or just include it for everyone, without any flags.

The current setup is leading people to make (in my opinion, bad) suggestions to overcomplicate instructions e.g. at https://github.com/leanprover-community/leanprover-community.github.io/pull/487/files

[Utensil Song]

Most users of leanblueprint would need doc-gen4 locally, and even if it's only run in CI, since CI shares the same manifest with local development, a user runs lake update locally will destroy CI too (it happens every once a while someone forgets this caveat).

[Utensil Song]

If you are suggesting that people should start requiring doc-gen4 without the condition, I agree, because it's just a (nowadays not so applicable) convention that's followed along.

[Utensil Song]

My comments in the PR merely explain the status quo for formalization projects, and such longer one-liner is necessary for now, but I'm definitely happy to see the situation change, i.e. maybe in the default lakefile generated by leanblueprint could use unconditional require.

But this was not really a deliberate design choice for leanblueprint, only something followed along from the early days that doc-gen4 wishes to be a non-mandatory dependency. It was not a bad thing to do so in other package management systems, e.g. pip, node.js, rust etc. only that it's causing issues for lean/lake users because this conditional requiring is not part of the standard and has surprising consequences.

[Utensil Song]

To make the situation more complicated, I've also seen projects using -Kenv=ci and even -Kdoc=on for conditionally requiring doc-gen4.

[Kim Morrison]

I would love to see leanblueprint, and the maintainers of the large projects using it, removing these conditional requires and making life sane for their users.

Also note that in the medium term we would like to remove meta if, or at least discourage users from using it at all, in favour of the new lake install for dev tools.

[llllvvuu]

If you upgrade doc-gen4 from dev dependency to dependency will that make downstream packages also get doc-gen4 as a dependency?

(A nice thing about dev dependencies in npm is that npm install installs your dev dependencies but not upstream dev dependencies)

[Kim Morrison]

Yes, lake install will do that too.

[Kim Morrison]

For now, I'm not sure if we have an example of a project using doc-gen4, and a downstream dependency not using doc-gen4, and it that is the case I'd prefer we don't make things complicated just for hypotheticals!

[Utensil Song]

Yes, it would be nice to see a standard way to declare an optional dependency, that would always be seen by lake and handle accordingly, unlike the meta if making lake not seeing it sometimes and behavior surprisingly.

[Utensil Song]

For now, it's pretty safe to assume downstream of a project using doc-gen4 would not worry about some unused extra packages.

[Patrick Massot]

I have no opinion about that discussion. @Kim Morrison if you know what should be done for blueprints then I will happily merge a PR from you in the leanblueprint repo.

[Yaël Dillies]

Am I right that the outtake of this discussion is that lake update -R -Kenv=dev is necessary until lake install becomes a thing?

[Utensil Song]

Yes, or until leanblueprint starts producing unconditional doc-gen4 requiring, and all existing formalization projects are PRed to do the same, as the old lakefiles are there to cause issues once generated.

[Utensil Song]

And actually I don't think it's a bad one-liner compared to curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none that everyone is already used to.

[Yaël Dillies]

Hmm, actually I never had to use that one(-liner)

[Utensil Song]

It's definitely a better idea to include a simple script generated by leanblueprint to bump mathlib (until the situation is changed).

[Utensil Song]

Yaël Dillies said:

Hmm, actually I never had to use that one(-liner)

What did you use (for installing elan) ?

[Yaël Dillies]

It already comes installed in my gitpod workspace

[Utensil Song]

Yaël Dillies said:

It already comes installed in my gitpod workspace

which in turn uses the one-liner in the Dockerfile.

[Kim Morrison]

The thing I don't understand in this discussion is why we can't have a conditional doc-gen4 require, but no human ever turns it on, thereby removing the need for -Kenv=dev (or -R, which ideally would never have existed in the first place).

[Kim Morrison]

doc-gen4 should only be run by CI, and that can take care of using -K.

[Kim Morrison]

This is, after all, what Mathlib does, and I don't understand why it is any different for downstream projects.