can doc-gen4 show sorry-dependency?

Stream: general

[Malvin Gattinger]

Is there a way to get the information "this theorem currently (transitively) depends on sorryAx" into the doc-gen output, i.e. the documentation website? I imagine something like a :check: or :thinking: next to the name of the theorem.

For mathlib this does not matter of course as it shall never have anything depending on sorryAx, but for a separate project I would like to have this and could not find any similar discussion.

[Damiano Testa]

Do you want it specifically for doc-gen, or having a linter that flags this would be enough?

[Damiano Testa]

There was a previous discussion of flagging Classical.choice, but you can equally well flag any other axion, such as sorryAx.

[Damiano Testa]

The linter is here: #lean4 > restricting axioms @ 💬.

[Malvin Gattinger]

Thanks, that linter might be useful too, but I am still interested in specifically doc-gen. My use case is that from a (non-Lean) math article I want to link to things in the doc-gen and there people should instantly be able to see whether this thing is already fully verified or not.

[Damiano Testa]

The linter can help maintain this in sync, for instance, the linter could emit a warning only of the doc-string does not contain "Depends on sorry." as a substring.

[Damiano Testa]

But to make this fully automated would require a little more infrastructure.

[Malvin Gattinger]

Hm, okay. I want to avoid manually updating this information - if one finishes the last sorry in a proof this is still manageable for that theorem itself, but not for all stuff depending on it.

In my experiment to get automated Lean cehcks into tex files here https://github.com/m4lvin/RepLeanTeX I also used the #print axioms method, I was hoping something similar could be done with doc-gen.

How much is "more infrastructure" here? I assume the doc-strings already get evaluated somehow for example to linkify identifiers in code. Would DocGen4.Process.TheoremInfo be the right place to start messing around with this if I ever feel like it?

[Damiano Testa]

Oh, I do not know about the doc-gen infrastructure. I was more thinking of automating the adding/removing of a comment in the doc-string.

[Damiano Testa]

Since the linter gives you exact location where the comment is/isn't, you can build a small script on top of that that acts on the linter warning.

[Damiano Testa]

I am not saying that this is a principled way, but I have written a few "automatic linter-guided modifications" and they worked very well.

[Eric Wieser]

Does doc-gen4 currently indicate theorems which directly use sorry?

[Eric Wieser]

(I remember implementing this in Lean 3, but we never had the transitive version there)

[Malvin Gattinger]

Eric Wieser said:

Does doc-gen4 currently indicate theorems which directly use sorry?

As far as I can see, no. An example is here which includes a sorry here.

[Malvin Gattinger]

Getting both pieces of information would be even nicer, e.g. a bold red sorry if it uses sorry directly, and a light orange one if transitively.

I am surprised that for Lean 3 only the direct use was implemented, isn't that harder to do (because one needs to inspect the proof term I guess?) than the transitive check (as done by e.g. #print axioms)?

[Malvin Gattinger]

Related to this, I also found very useful the #axiom_blame tool made and discussed here. Now imagine the doc-gen output could even show where the sorry comes from :)

[Jz Pan]

Maybe blueprint can do this?

[Eric Wieser]

I think we should just add this feature to doc-gen. https://github.com/leanprover-community/doc-gen/pull/149 was the PR that added it to Lean 3.

[Kevin Buzzard]

Malvin Gattinger said:

Eric Wieser said:

Does doc-gen4 currently indicate theorems which directly use sorry?

As far as I can see, no. An example is here which includes a sorry here.

This example definitely has a sorry but yes there seems to be no mention in doc-gen

[Malvin Gattinger]

Wait, Wiles_Taylor_Wiles has no sorry in its proof term as written there, right? It just depends on something that uses sorry. As far as I understand the code from the Lean 3 PR Eric linked to above, it only flagged things with an "immediate" sorry, and not things that transitively depend on something with sorry.

[Kevin Buzzard]

Yes, the proof itself has no sorry but it uses many things which have sorrys

[Kim Morrison]

Would someone like to create an issue at doc-gen4 to track this?

I think this would be a great feature, and would encourage someone to implement it! :-)

[Malvin Gattinger]

I can try to write an issue, based on the discussion here. Is it okay to include both "uses sorry directly" and "transitively depends on sorry" in the same issue or should those be separate ones?

[Kim Morrison]

Let's just have one issue.

[Malvin Gattinger]

I've added an issue now, and included some mock-ups how it could look like: https://github.com/leanprover/doc-gen4/issues/270