Re: [isabelle] Troubleshooting a nondeterministic SMT failure



On 18/11/2021 15:31, Brandon Bohrer wrote:
> 
> I actually have already tried setting high
> timeouts as well (e.g. declare[[smt_timeout=10000]]) but did not mention that
> explicitly in my first email because all of the successful smt calls and all
> of the failing smt calls complete quite quickly (e.g. 0.2 seconds). Note that
> things are failing on my faster machine and succeeding on my slower machine.
> 
> By the way, I also tried declare[[smt_timeout=0]] right now, just in case (on
> the Isabelle2021 release, not an RC). The result was that it set the timeout
> to 0 seconds rather than infinity, so that all of the smt calls fail every
> time. At least that's a deterministic behavior, so maybe it's an improvement :)

The smt_timeout behaviour changed shortly after the Isabelle2021 release, so
in Isabelle2021-1 release candidates it observes the common scheme of Isabelle
tools that 0 means infinity (actually anything < 1ms).

See also these history items:

https://isabelle.sketis.net/repos/isabelle/rev/a40e69fde2b4

https://isabelle.sketis.net/repos/isabelle/rev/f3378101f555


The timeout_scale mentioned there is explained in the NEWS for Isabelle2021-1
as follows:

* 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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.