Stream: Mirror: Isabelle Development Mailing List

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


view this post on Zulip Email Gateway (Oct 12 2023 at 20:06):

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

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: Mar 04 2024 at 10:08 UTC