Re: [isabelle] Troubleshooting a nondeterministic SMT failure



Dear Makarius,

Thanks for the follow-up, that definitely clears up my misunderstanding of Mathias' earlier email. I don't have any of the RCs installed at the moment, but if I'm reading the news correctly, I expect that my original issue would be unchanged if I run an RC.

Changing timeouts was one of the troubleshooting steps I tried and timeouts did not appear to be the issue. Since I'm on the 2021 release, I set the timeout to 10000 seconds (~2 hours) rather than setting the value to 0, and the SMT calls in question finished in well under a second, both the successful and unsuccessful calls. No timeouts occur on the default setting, nor when I increase the timeout limit.

Taking that into consideration, I would be happy to hear from anyone whether it makes sense to install and test an RC (or nightly) build. For example, if there are major SMT communication protocol changes other that the timeout handling, then I think testing the latest version would still make sense.

Thanks again everyone for the troubleshooting help,
-Brandon



On Sat, Nov 20, 2021 at 6:46 AM Makarius <makarius at sketis.net> wrote:
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.