Zulip Chat Archive

Stream: lean4

Topic: Success is not monotone in `synthInstance.maxSize`


Eric Wieser (Jan 03 2025 at 23:07):

I'm in a situation where synthInstance.maxSize = 128 fails, but both 127 and 130 work. Wouldn't the expected behavior be that for any given problem, it succeeds until a certain limit, then fails everywhere below it?

import Mathlib

open Nat

set_option synthInstance.maxSize 128 -- the default; change to 127 and it works

abbrev broken :=  n : ,
  let bin := [1] ++ (digits 2 n) ++ [1];
  Decidable <|
     i j : Fin bin.length, i < j  bin.get i = 1  bin.get j = 1 
      ( k, i < k  k < j  bin.get k = 0)  Even ((j : ) - (i : ) - 1)

#synth broken

(cc @George Tsoukalas whose code this is extracted from)

Eric Wieser (Jan 03 2025 at 23:18):

Frustratingly it seemingly becomes monotone just after the default limit!

run_meta do
  let fails  (List.range 500).filterM fun x => do
    withOptions (fun o => Lean.Meta.synthInstance.maxSize.set o x) do
      let s  getThe Meta.State
      try
        return ! (succeeds (synthInstanceQ q(broken)))
      finally
        set s  -- ensure the result isn't cached
  Lean.logInfo m!"{fails}"
  guard <| fails = List.range 22 ++ List.range' 30 6 ++ List.range' 63 4 ++ List.range' 128 2

Last updated: May 02 2025 at 03:31 UTC