Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] ML: distinguish proper interrupts from Pol...

Email Gateway (Oct 12 2023 at 20:06):

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

• Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML
  runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error.
  Exn.is_interrupt covers all kinds of interrupts as before, but
  Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more
  specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.

This refers to Isabelle/280a228dc2f1.

Here is an artificial example:

ML ‹fun bad () = (Isabelle_Thread.expose_interrupt (); 1 + bad ())›

ML_val ‹Timeout.apply_physical (seconds 0.1) bad ()› (Timeout after 0.100s)
ML_val ‹Timeout.apply_physical (seconds 0.5) bad ()› (Timeout after 1.866s)
ML_val ‹Timeout.apply_physical (seconds 1.0) bad ()› (Timeout after 2.118s)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()› (*exception
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()› (Timeout after 4.546s)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()› (*exception
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()› (*exception
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)

This shows that the result is a bit non-deterministic. It remains to be seen
how usable it is in realistic applications.

Makarius

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

Last updated: Apr 27 2024 at 20:14 UTC