Re: [isabelle] Isabelle2015-RC3 available for testing



Dear Alfio,

> - Isabelle for Windows: Using the standard configuration,  s/h
>   solves the first lemma only with e (and it takes quite some time
>   to do it).

Thatâs really bad â that lemma is supposed to be ultra easy. In a previous email, I suggested you try disabling MaSh. Did that make any change?

Otherwise, thanks to my colleague Mathias Fleury, we should be able to include CVC4 executables with proof output in RC4 and/or the final Isabelle2015 release. We will look into this in the next 24 hours. Makarius, please donât release anything until then. ;)

Weâll also see if we manage to reproduce the issues. I unfortunately have no Windows license anymore now that Iâve left the TU MÃnchen, so I need to find a solution quick or rely on your remote debugging. If you think this could be useful, we could try a chatting session. Otherwise, I could try pestering my Windows-based students. ;)

Cheers,

Jasmin





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