show direct usage of sorry and dependency on sorryAx in the docs

[m4lvin]

It would be nice to mark definitions and theorems that

• directly use sorry, or

• (transitively) depend on something that uses sorry, i.e. depend on the sorryAx axiom.

This does not matter for mathlib, but other projects will often generate docs for (currently) partial formalizations, e.g. FLT. My personal use case is lean4-pdl.

I think both things should be visible but also not take up too much space. For direct use of sorry it might be nice to use the same style as in VS code, i.e. squiggly underline. For transitive depending on sorry then maybe a dashed line? Or something even smaller or subtle.

For example, the following code

theorem direct p : p → ¬ p := by intro h; sorry

theorem depends : False := direct True trivial trivial

could lead to the following documentation (mock-up):

And there could be mouse-over tooltips (using the HTML title attribute) to explain what the marking means:

Related:

• Zulip discussion

• PR that added direct sorry markers to doc-gen for Lean 3 by @eric-wieser