Profiling simp

Stream: lean4

[Bolton Bailey]

I have set_option profiler true to try to find out why my code is so slow. I got the output

simp took 225ms
simp took 469ms
simp took 285ms
simp took 6.03s
simp took 41.9s
type checking took 4.04s
elaboration took 18.5s

for my proof

lemma Marlin_numCommitments (F : Type) [field_F : Field F] [fintype_F : Fintype F] [DecidableEq F] [Inhabited F] (ω : F) (n_stmt n_wit m : ℕ)
    (r : (Matrix (Fin (n_stmt + n_wit)) (Fin ((n_stmt + n_wit))) F)) :
    (MarlinProofSystem (F := F) ω n_stmt n_wit r).numCommitments = 1029 := by

  simp_rw [MarlinProofSystem, Marlin, ProofSystem.fromIOPMonad]

  simp only [commitment_counter_PolyCommitIOPMonad]

  simp only [RowCheck, LinCheck, SumCheckToZero, SumCheckTo, MatrixCommit, SendFieldElement]

  simp only [bind_assoc, SquareR1CS.default_def]

  done

[Bolton Bailey]

Why are there five different simp times when there are only four calls? Which times map to which calls?

[Damiano Testa]

Could it be that simp_rw counts as 3 calls and only two of them are slow enough to trigger a trace mention?

[Kevin Buzzard]

set_option trace.profiler true might give you the information you need.

[Ruben Van de Velde]

Damiano Testa said:

Could it be that simp_rw counts as 3 calls and only two of them are slow enough to trigger a trace mention?

Likely that, yeah. simp_rw is just a sequence of simp only calls