Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] printing debug info from generated code execut...

Email Gateway (Feb 24 2022 at 12:29):

From: Peter Lammich <lammich@in.tum.de>
Hi,

to debug a functional program implemented in Isabelle/HOL, I naively
tried to insert print-statements (as I would do with @{print} in
Isabelle-ML). The PolyML approach would be

definition "print x = x"
code_printing
constant print ⇀ (SML) "(PolyML.print)"

definition "dummy ≡ print (0::integer)"

value dummy
ML_val ‹
@{code dummy}
›
*** fails, PolyML.print not available

However, I learned that since 2016-1, "Low-level ML system structures
(like PolyML and RunCall) are no longer
exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.

Also, if I use the same approach as @{print} or @{make_string}, via
ML_system_pretty, I only get the output "?" instead of the expected
"0".

Is there any way to get back a similar functionality, that would
convert values of any type into some more or less readable string/trace
output. As I only want to use it for debugging, the output strings need
not be precise or clean or whatsoever.

Email Gateway (Feb 24 2022 at 22:10):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Peter,

Are you aware of HOL-Library.Debug? This theory defines a constant
flush and code_prints it to Output.tracing in the Eval target. IIRC
the @{code} antiquotation uses the code target Eval; if not, you'd have
to redo the code_printing declarations for SML.

Hope this helps,
Andreas

Last updated: Jul 15 2022 at 23:21 UTC