Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] *** exception ValueMissing raised

view this post on Zulip Email Gateway (Aug 18 2022 at 11:44):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
I'm using a very recent version of Isabelle, and I get the message

*** exception ValueMissing raised

I can't find such an exception anywhere in the source code.

What does it mean, and where does it come from?

Thanks,

Jeremy

view this post on Zulip Email Gateway (Aug 18 2022 at 11:44):

From: Makarius <makarius@sketis.net>
This exception appears in Poly/ML at least until 5.0 (I did not check 5.1;
it is absent in recent development versions of Poly/ML 5.2).

To get an idea where the problem originates just do

ML_command {* set Toplevel.debug *}

and look at the raw output (in the isabelle buffer of Proof General).

Sometimes you may have to wrap suspicious code into PolyML.exception_trace
to get to the point.

Makarius

Last updated: May 03 2024 at 08:18 UTC