timeout manipulating proof terms (e.g. whnf)

Stream: general

[Gabriel Poesia]

Hey! I'm using metaprogramming to analyze proof terms from mathlib, and simple manipulations in some of them seem to often cause timeouts. But these timeouts seem to be independent of that - just typechecking these terms by putting them in standalone files also doesn't work. Here is an example:

import Mathlib

open IntermediateField

theorem instIsCompactlyGenerated2.{u_1, u_2} : ∀ {F : Type u_1} [inst : Field F]
  {E : Type u_2}
  [inst_1 : Field E] [inst_2 : Algebra F E], IsCompactlyGenerated (IntermediateField F E) := fun {F} [Field F] {E} [Field E] [Algebra F E] =>
  by exact {
    exists_sSup_eq := fun s =>
      Exists.intro ((fun x => F⟮x⟯) '' ↑s)
        ⟨fun t a =>
          Exists.casesOn a fun x h =>
            And.casesOn h fun left right => right ▸ IntermediateField.adjoin_simple_isCompactElement x,
          Eq.trans sSup_image
            (Eq.trans (IntermediateField.biSup_adjoin_simple ↑s)
              (_root_.le_antisymm (IntermediateField.adjoin_le_iff.mpr le_rfl)
                (IntermediateField.subset_adjoin F ↑s)))⟩ }

Running this file gives me (deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached (on v4.24.0-rc1). This term in particular is generated for a typeclass instance, but if it helps I have other small examples.

The practical case for me happens when trying to iterate over thmInfo constants, converting their values into Canonical's Term representation (which involves traversing the term and calling whnf and inferType), and then creating a dataset out of that. The current goal is to build a simple data structure to help guide proof search in Canonical. But since these timeouts are reproducible independently of Canonical, I wonder if it's unstable to do much with mathlib proof terms outside of the kernel besides just processing them syntactically (e.g., traversing them as Expr). Is that expected to happen?

[Ruben Van de Velde]

To be clear, you're serialising proof terms into explicit lean code and reparsing it? I wouldn't be particularly surprised that that goes wrong

[Gabriel Poesia]

In the actual use case I'm just trying to call Canonical.toTerm on proof terms I get directly from the global context (so not reparsed). toTerm mostly relies on whnf and inferType while traversing the term. The file above is just a case where this times out, and yes, that's a case where printing and reparsing also times out (perhaps for similar underlying reasons?)

[Aaron Liu]

Does it work if you make everything explicit