Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



On 27/05/2019 13:58, Fabian Immler wrote:
> 
> But I realized that Windows' "Virus & threat protection" seems to be the
> culprit.
> 
> When building the theory with 400 smt calls, Task Manager shows that
> "Antimalware Service Executable" is very active (100-150% CPU).
> 
> Disabling it temporarily
> (Virus & threat protection ->
> Virus & threat protection settings ->
> Mange settings ->
> Real-time protection), the problems with smt disappear.

I have experimented with this a bit. Using 500 copies of your example
(as in the included compressed Test.thy), I see approx. 2 errors on one
of my Windows 10 test machines.

In the Windows Defender Settings there is a section "Virus & threat
protection settings". The second-last item at the bottom is for
"Exclusions". Here I have added the whole Isabelle home directory (as
over-approximation of all Isabelle components, cygwin bash etc.).

This appears to help: in a few subsequent tests there were no errors.


	Makarius

Attachment: Test.thy.gz
Description: application/gzip



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