HomeIsabelle/Phabricator
Clarified timeouts for Isabelle/ML tools

General

  • Timeouts for Isabelle/ML tools are subject to system option timeout_scale --- this already used for the overall session build process before, and allows to adapt to slow machines. The underlying Timeout.apply in Isabelle/ML treats an original timeout specification 0 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY in boundary cases.

This refers to Isabelle/3b5196dac4c8.

Written by makarius on Mar 5 2021, 10:29 PM.
User
Projects
None
Subscribers
None

Event Timeline