isDefEq deterministic timeout

Stream: lean4

[Jovan Gerbscheid]

I ran into a problem where isDefEq does a deterministic time-out, when it should fail. Here is a minimal example:

open Lean Meta Expr
#eval show MetaM _ from do
  let ringNat ← mkFreshExprMVar (Expr.app (.const ``StrictOrderedRing [.zero]) (.const `Nat []))
  let lhs := .app
    (.app (.const `Filter.atTop [.zero]) (.const `Nat []))
    (.app
      (.app (.const `PartialOrder.toPreorder [.zero]) (.const `Nat []))
      (.app
        (.app
          (.const `StrictOrderedSemiring.toPartialOrder [.zero])
          (.const `Nat []))
        (.const
          `Nat.strictOrderedSemiring
          [])))
  let rhs := .app
    (.app (.const `Filter.atTop [.zero]) (.const `Nat []))
    (.app
      (.app (.const `PartialOrder.toPreorder [.zero]) (.const `Nat []))
      (.app
        (.app (.const `StrictOrderedRing.toPartialOrder [.zero]) (.const `Nat []))
              ringNat))
  logInfo m! "{← isDefEq lhs rhs}"

which gives

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Clearly, Nat is not a ring, so it should fail the unification.

[Mauricio Collares]

#mwe?

[Jovan Gerbscheid]

Ah, sorry. Here it is:

import Lean
import Mathlib

open Lean Meta Expr
#eval show MetaM Bool from do
  let ringNat ← mkFreshExprMVar (Expr.app (.const ``StrictOrderedRing [.zero]) (.const `Nat []))
  let lhs := .app
    (.app (.const `Filter.atTop [.zero]) (.const `Nat []))
    (.app
      (.app (.const `PartialOrder.toPreorder [.zero]) (.const `Nat []))
      (.app
        (.app
          (.const `StrictOrderedSemiring.toPartialOrder [.zero])
          (.const `Nat []))
        (.const
          `Nat.strictOrderedSemiring
          [])))
  let rhs := .app
    (.app (.const `Filter.atTop [.zero]) (.const `Nat []))
    (.app
      (.app (.const `PartialOrder.toPreorder [.zero]) (.const `Nat []))
      (.app
        (.app (.const `StrictOrderedRing.toPartialOrder [.zero]) (.const `Nat []))
              ringNat))
  isDefEq lhs rhs

[Gareth Ma]

:joy:

[Mauricio Collares]

(deleted)

[Mauricio Collares]

You can type set_option trace.Meta.synthInstance true and set_option trace.profiler true to see what Lean is trying.

[Mauricio Collares]

(deleted)

[Jovan Gerbscheid]

I tried using set_option maxHeartbeats 1000000, and now after almost a minute, it successfully returns false. set_option trace.profiler true indeed shows what Lean is trying, but it doesn't help me much. I suppose I shouldn't trust that all definitions in Mathlib are handled well by isDefEq. Instead, is there a good way to limit the run time taken by isDefEq? I'm working on an interactive program, so I need it to run near instantaneously.

[Gareth Ma]

Instead, is there a good way to limit the run time taken by isDefEq?

Isn't that what maxHeartbeats does?

[Kyle Miller]

It looks like Aesop wanted a similar thing, so there's docs#Aesop.withMaxHeartbeats to limit a sub-computation. It doesn't let you know if the result failed specifically due to the heartbeat limit however.

[Jovan Gerbscheid]

Kyle Miller said:

It looks like Aesop wanted a similar thing, so there's docs#Aesop.withMaxHeartbeats to limit a sub-computation. It doesn't let you know if the result failed specifically due to the heartbeat limit however.

Thanks, that should do the job.

[Jannis Limperg]

There is also the extremely hacky docs#Lean.Exception.isMaxHeartbeat for figuring out whether an exception is due to a deterministic timeout.