Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Plan for Isabelle2021 release


view this post on Zulip Email Gateway (Sep 25 2020 at 14:22):

From: Makarius <makarius@sketis.net>
Quote from https://isabelle-dev.sketis.net/phame/post/view/21

"""
The next anticipated release is Isabelle2021 (February 2021). The hot phase
with release candidates will presumably be 28-Dec-2020 .. 15-Feb-2020.
"""

Thus it is 10 months after Isabelle2020, according to our standard scheme. It
also means that for the year 2021 we shall have a second release on 15-Dec-2021.

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 have not yet started to sort out my own TODO list, but would definitely like
to add a few things to Isabelle/jEdit, e.g. integrated support for repository
browsing.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 28 2020 at 08:25):

From: Jasmin Blanchette <j.c.blanchette@vu.nl>
Hi Makarius,

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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 28 2020 at 09:30):

From: Lawrence Paulson <lp15@cam.ac.uk>
This certainly looks worth doing!
Larry


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 28 2024 at 12:29 UTC