speed up Print Assumptions: walk stored proof term

[zeldovich]

This change speeds up Print Assumptions for large proofs that have a lot of shared terms. The motivation was a large Iris-based project where [Print Assumptions] on a single top-level theorem was almost half of the total build time of the whole project (6 minutes out of 13 minutes).

[Print Assumptions] obtains every opaque body through [Global.force_proof], which applies the section discharge ([Discharge.cook_opaque_proofterm], once per enclosing section) before the command looks at the term. The discharge is a rebuild, and the rebuild destroys sharing.

complexity/PrintAssumptionsSharing.v is a regression test for the walk itself: a proof whose stored DAG is 22 nodes and whose tree unfolding is over 4M, so the old walk is exponential in the size of the file.

This also adds a test for the weird corner case of [Print Assumptions] that wasn't covered by existing tests (the "used in" annotation that [ax2ty] attaches to an axiom eliminated by a [match ... with end]).

[SkySkimmer]

This is a user visible change

Axiom f : False.

Definition bla := (let x := nat in match f return x with end, let y := bool in match f return y with end).

Print Assumptions bla.
(* master:
Axioms:
f : False
used in bla to prove
 y
used in bla to prove
 x

PR:
Axioms:
f : False
used in bla to prove
 x
*)

but IDK if that really matters considering y and x are not very informative without printing the local context.

[JasonGross]

If you do Require Import Coq.Compat.AdmitAxiom. and then admit a handful of sub goals, does this make it so that only one appears?

[zeldovich]

I pushed a commit to preserve the old behavior. (I had assumed this is some weird feature that's not used, but clearly that's not true.) The fix is to avoid caching anything that produces one of these "used in" reports.

[JasonGross]

See #4300 , #4054 , 2defd4c for the history. (tl;dr: the move to the new evar-based proof engine in 8.4->8.5 made it infeasible to mint global axioms during proof execution, so admit became abstract case proof_admitted for proof_admitted : False; later support was added to fix Print Assumptions)