Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Clarified timeouts for Isabelle/ML tools

Email Gateway (Mar 05 2021 at 21:32):

From: Makarius <makarius@sketis.net>
* 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.

Application: smt_timeout = 0 (unlimited) in Isabelle/f3378101f555.

Makarius

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

Last updated: Apr 19 2024 at 01:05 UTC