Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Robust handling of program exception...

view this post on Zulip Email Gateway (Sep 29 2023 at 12:24):

From: Makarius <>
* ML *

See also the implementations Isabelle_Thread.try_catch / try_finally /
try. The HANDLER always runs as uninterruptible, but the EXPR uses the
the current thread attributes (normally interruptible). Various examples
occur in the Isabelle sources (.ML and .thy files).

This refers to Isabelle/fc0814e9f7a8 and AFP/9c5fe84ef108.

Instead of friendly hints in the "implementation" manual (which still needs to
be updated), there are now hard checks in the Isabelle/ML compiler setup and
proper antiquotations to get things right by construction.

This is only the first stage of a substantial reform in exception handling.
The next stage will be distinct Exn.Interrupt_Break (interactive thread
signal) vs. Exn.Interrupt_Breakdown (resource problem in the ML runtime-system).


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC