Stream: Mirror: Isabelle Development Mailing List

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

Email Gateway (Sep 29 2023 at 12:24):

From: Makarius <makarius@sketis.net>
* ML *

• ML antiquotation "try" provides variants of exception handling that
  avoids accidental capture of physical interrupts (which could affect ML
  semantics in unpredictable ways):

  \<^try>‹EXPR catch HANDLER›
  \<^try>‹EXPR finally HANDLER›
  \<^try>‹EXPR›

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).

• Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
  INCOMPATIBILITY, better use \<^try>‹...› with 'catch' or 'finally', or
  as last resort declare [[ML_catch_all]] within the theory context.

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).

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 28 2024 at 12:28 UTC