[isabelle-dev] Plan for Isabelle2021 release

[Lawrence Paulson]

This certainly looks worth doing!
Larry

> On 28 Sep 2020, at 09:25, Jasmin Blanchette <j.c.blanchette at vu.nl> wrote:
> 
> I don't think it should influence the schedule, but Isabelle2021 would be high time to repackage new versions of the automatic theorem provers and new provers -- and make sure that things work smoothly with Sledgehammer.
> 
> Main provers to update:
> 
> 	E
> 	Vampire
> 	CVC4
> 
> New provers:
> 
> 	veriT
> 	Zipperposition
> 
> All of these now partly or fully support higher-order logic. The main bottleneck here is that I've lost my Windows installation and I need to do something about this very soon (i.e., find somebody else who can own that problem or reinstall Windows myself).
> 
> (On a related note, Martin D. has recently updated Metis's source code, which is nice because Metis had some completeness bugs. We don't know if it affected Isabelle users but that could have explained why it sometimes went seemingly forever on seemingly easy goals.)