Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML stack trace?

view this post on Zulip Email Gateway (Aug 18 2022 at 10:20):

From: Tao Ma <separable@gmail.com>
hi,
i would like to find out more information when the isabelle gives "empty
result sequence".
it seems this exception is raised by a line proof_history.ML, so i tried to
use polyml
debugger to set a breakpoint, recompile the source adding
Poly.Compiler.debug := true
then in proof general use "ML {* open PolyML.Debug; breakAt
(proof_history.ML 70); *}"
but it doesnt seem to work. is there a way to get the stack trace?
thanks
tao

Last updated: May 03 2024 at 04:19 UTC