Email Gateway (Nov 26 2021 at 20:14): Email Gateway (Nov 26 2021 at 20:14):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
we now have the pre-final release candidate
https://isabelle.sketis.net/website-Isabelle2021-1-RC4 and AFP has also moved
to official ssh://hg@foss.heptapod.net/isa-afp/afp-2021-1
See again the blog entry
https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
for details.
I have reworked many details of HTML presentation and LaTeX document
preparation: normally this is not the time for new features, but a few
important things were still in the pipeline.
We have now approx. 2 weeks left until final lift-off (before 15-Dec-2021). So
this is the last chance to figure out problems and solutions, before the
release becomes immutable.
Reminder: Any feedback about release candidates should be posted with a meaningful
Subject (not just a clone of the announcement).
Makarius
Email Gateway (Nov 26 2021 at 21:24):From: Peter Lammich <lammich@in.tum.de>
Hi,
Simon just has fixed a regression introduced into
AFP/Refine_Imperative_HOL, by enforcing context discipline, but not
fixing all places where this new behaviour caused errors.
@Simon: can you submit the patch ASAP?
Email Gateway (Nov 27 2021 at 14:06):From: Simon Wimmer <wimmersimon@gmail.com>
Hi,
the patch is now on afp-devel (
https://foss.heptapod.net/isa-afp/afp-devel/-/commit/27b8976bf077f9dcd9c4f5b5d6ccae4ca872fd1a
)
and attached to this email.
I second that it would be important to have it in the release of afp-2021-1.
Simon
sepref.patch
Email Gateway (Nov 28 2021 at 03:07):From: Gerwin Klein <kleing@unsw.edu.au>
Thanks, I will add it to afp-2021-1.
Please do let me know in general if any afp-devel changes should go into the release version. By default any changes in afp-devel will be ignored for the release.
Cheers,
Gerwin
Email Gateway (Nov 28 2021 at 03:09):From: Gerwin Klein <kleing@unsw.edu.au>
(now added)
Gerwin
Last updated: Jan 04 2025 at 20:18 UTC