Stream: Isabelle/ML

Topic: Can you capture the simp trace from Isabelle/ML ?

Andrea Vezzosi (Feb 10 2025 at 17:46):

Hi, I am using Goal.prove_common to prove a goal with auto_tac and I would like to report which lemmas were used during simplifcation, I figured if I enabled simp_trace there might be a way to collect it and I could parse the info from there?

Yutaka Nagashima (Feb 12 2025 at 01:17):

Hi @Andrea Vezzosi ,

I don't really know much about simp_trace.
But the usual step would be something like

• 1: check the ML source code of the command,
• 2: find the relevant ML functions, and
• 3: run them.

I've done this loads of times over the past 10 years, and it's always been great fun!
:laughing:

Andrea Vezzosi (Feb 18 2025 at 15:24):

Oh, sure! Btw the solution was to hijack the tracing_fn mutable reference that controls where tracing output goes.
Unsynchronized.setmp Private_Output.tracing_fn <fun writing input to ref> <do the proving, read trace from ref> ()

Yutaka Nagashima (Feb 21 2025 at 18:30):

Stay safe from concurrency. :bird:

Last updated: Apr 18 2025 at 20:21 UTC