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

[Malvin Gattinger]

I tried my luck looking into the doc-gen4 codebase to make this feature happen. Here is my attempt https://github.com/leanprover/doc-gen4/compare/main...m4lvin:doc-gen4:show-sorryAx with which lake build in doc-gen4 itself works fine, but for some reason lake build DocGen4:docs now takes really loooong. I have processes with genCore Lean and genCore Std that seem to take forever, whereas before it took less than 8 minutes. Is there something cached online normally that could take very long? Or is the place and way that I added collectAxioms too naive and leading to some sort of infinite loop? :thinking:
Thanks for any help and advice! (I also hope to make a PR of course, but first wanted to at least get it working locally.)

[Henrik Böving]

You're running collectAxioms for every name seperately so you are going to run into a lot of overhead because if a name is used in n declarations it will be checked at least n times + all of the uses of those declarations and so on. You could try to add a cache here to stop revisiting the names over and over again but even then doing this will have significant computational impact as you can't cache results across modules given that they are worked in different processes.

[Malvin Gattinger]

Right, that makes sense, thanks! I assume this is why in the Lean 3 version we also only had a marker for "uses sorry directly" and not for "depends on sorryAx"?

[Henrik Böving]

I don't know, doc-gen3 was a completely different code base. If doc-gen was engineered to work in one process with multiple threads instead having a cache shared between these threads would very much be possible

[Malvin Gattinger]

Putting aside the difficult isse of marking transitive dependency on sorry, I now managed to at least mark direct uses of sorry, see doc-gen4#319 and this example what the result looks like.

[Chris Henson]

Would it make sense for proof_wanted to appear similarly? That could be relevant to Mathlib. (I don't believe they appear in docs at all at the moment, so that is perhaps a prerequisite conversation).

[Malvin Gattinger]

It seems indeed proof_wanted entries do not appear at all in the docs at the moment, I do not know how difficult it would be to make them appear. I also think they should not appear very similarly, given that a sorry-using statement can already be used but a proof_wanted cannot (so it would maybe also be misleading to make them appear in the search). On the other hand I guess making proof_wanted appear in the docs might prevent someone from reinventing its statement and name.

[Chris Henson]

I'm not familiar with doc-gen4 internals, but it might be awkward to include for a couple of reasons:

• proof_wanted is defined in Batteries
• it elaborates using docs#Lean.withoutModifyingEnv

[Henrik Böving]

That makes it doubly impossible to add