Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tracing the simplifier in proofs

view this post on Zulip Email Gateway (Aug 18 2022 at 12:42):

From: John Matthews <matthews@galois.com>
Hi,

I would like to be able to trace a particular call to the simp method
within a proof, without having to manually turn tracing on and off
from the ProofGeneral menu. This is because half the time I forget to
turn tracing back off when I'm replaying earlier parts of my theory,
and then PG gets swamped trying to display all the calls to the
various simp methods.

I tried this series of commands within my proof:

ML "trace_simp := true"
apply simp
ML "trace_simp := false"

but I get the following error from Isabelle when trying to execute the
first ML command:

*** Illegal application of command "ML" in proof mode
*** At command "ML".

So, what is the right way to be able to wrap calls to simp and auto
within proofs to turn on and off tracing?

Thanks,
-john

view this post on Zulip Email Gateway (Aug 18 2022 at 12:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,

I tried this series of commands within my proof:

ML "trace_simp := true"
apply simp
ML "trace_simp := false"

use "ML_val" instead of "ML"; "ML" is a theory-context sensitive
command and can only be used at the theory toplevel.

Note further that the Isabelle library provides set/reset combinators,
so just write

ML_val "set trace_simp"
apply simp
ML_val "reset trace_simp"

Hope this helps
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 12:42):

From: Makarius <makarius@sketis.net>
Either via the Proof General settings menu, or by issuing 'ML_command'
yourself, not 'ML'.

The reason why 'ML' did not work above is that it is now a theory command,
and cannot be used inside a proof. This is required because you would
usually expect to allow bind_thm inside 'ML' but that updates the theory.
In the next release even plain ML value bindings will affect the theory.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 12:42):

From: John Matthews <matthews@galois.com>
Thanks, Florian and Makarius. I'll switch to using ML_command in proofs.

-john

Last updated: May 03 2024 at 04:19 UTC