Skip to content
Started 9 mo 3 days ago
Took 2 hr 5 min on workermtahpc
Success

#2025 (Sep 30, 2023, 3:59:55 AM)

Build Artifacts
Changes
  1. moved variable bindings to tighter scope (detail / hgweb)
  2. removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer (detail / hgweb)
  3. removed unused function parameter (detail / hgweb)
  4. merged (detail / hgweb)
  5. A couple of new lemmas (detail / hgweb)
  6. merged (detail / hgweb)
  7. more NEWS; (detail / hgweb)
  8. explicitly reject 'handle' with catch-all patterns; (detail / hgweb)
  9. avoid accidental 'handle' of interrupts; (detail / hgweb)
  10. tuned: prefer try-catch/finally over low-level 'handle'; (detail / hgweb)
  11. clarified treatment of exceptions: avoid catch-all handlers; (detail / hgweb)
  12. clarified output vs. error: presence of error messages means error (see also cb7264721c91); (detail / hgweb)
  13. tuned; (detail / hgweb)
  14. more robust management of resources, using Thread_Attributes.uninterruptible; (detail / hgweb)
  15. tuned; (detail / hgweb)
  16. clarified signature; (detail / hgweb)
  17. more robust management of resources, using Thread_Attributes.uninterruptible; (detail / hgweb)
  18. tuned; (detail / hgweb)
  19. tuned; (detail / hgweb)
  20. tuned signature; (detail / hgweb)
  21. clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet); (detail / hgweb)
  22. clarified signature; (detail / hgweb)
  23. clarified modules; (detail / hgweb)
  24. unused; (detail / hgweb)
  25. clarified order of modules: early access to interrupt management of Isabelle_Threads; (detail / hgweb)
  26. tuned: prefer antiquotation for try-catch; (detail / hgweb)
  27. tuned: prefer antiquotation for try-catch; (detail / hgweb)
  28. tuned: prefer antiquotation for try-finally; (detail / hgweb)
  29. omit pointless capture/release (see also 469a375212c1); (detail / hgweb)
  30. omit pointless capture/release (see also 26774ccb1c74); (detail / hgweb)
  31. clarified signature: avoid association with potentially dangerous Exn.capture; (detail / hgweb)
  32. more robust: catch/finally part is uninterruptible; (detail / hgweb)
  33. more position information, e.g. for warning about fn-pattern; (detail / hgweb)
  34. unused; (detail / hgweb)
  35. more general ML_Antiquotation.special_form;
    more general "try" forms: support 'finally' or 'catch'; (detail / hgweb)

Started by an SCM change

This run spent:

  • 3 hr 9 min waiting;
  • 2 hr 5 min build duration;
  • 5 hr 14 min total from scheduled to completion.
Revision: a0f85118488cbfcd5a833ac512dbbcbaf4435be1