Hi Makarius,
> Are there any side-conditions to consider for the Isabelle2021 release
> schedule? What are important projects and tasks that need to be taken into
> account?
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.)
Cheers,
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
