Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Isabelle2022-RC3 with repository fork: Sun...

Email Gateway (Sep 30 2022 at 18:07):

From: Makarius <makarius@sketis.net>
The next release candidate (RC3) will coincide with the critical point of
forking isabelle-dev vs. isabelle-release, see also
https://isabelle.sketis.net/repos/isabelle-release

This is planned for Sunday 02-Oct-2022 12:00 UTC, i.e. 14:00 Bavarian time.

Afterwards, isabelle-dev will continue in post-release mode, but big changes
to the logic libraries should be avoided until afp-2022 is been forked from
afp-devel: Gerwin will say when this is done.

Any later changes to isabelle-release need to be significant, non-erratic, and
send to me via email (as result of "hg export" or "hg bundle").

Makarius

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

Email Gateway (Sep 30 2022 at 18:44):

From: Peter Lammich <lammich@in.tum.de>
... I'm still waiting for Florian (author of signed_divide change), or a
general OK such that I can factor out a syntactic signed_divide typeclass.

Or is the syntactic typeclass concept not wanted any more?

Email Gateway (Oct 01 2022 at 10:54):

From: Makarius <makarius@sketis.net>
OK. It is up to Florian to tell when he is finished with it.

Makarius

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

Email Gateway (Oct 01 2022 at 16:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Now done in a7ccb744047b.
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature

Email Gateway (Oct 02 2022 at 07:42):

From: Gerwin Klein <kleing@unsw.edu.au>
Thanks. With that, we’re ready to fork. I’ll do the AFP when Makarius has announced the Isabelle release fork.

Cheers,
Gerwin

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

Email Gateway (Oct 02 2022 at 18:37):

From: Makarius <makarius@sketis.net>

Am 01.10.22 um 12:54 schrieb Makarius:

On 30/09/2022 20:44, Peter Lammich wrote:

... I'm still waiting for Florian (author of signed_divide change), or a
general OK such that I can factor out a syntactic signed_divide typeclass.

OK. It is up to Florian to tell when he is finished with it.

Email Gateway (Oct 02 2022 at 18:38):

From: Makarius <makarius@sketis.net>
Done. See https://isabelle.sketis.net/repos/isabelle/rev/6ab4bb7cb8b2

Makarius

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

Email Gateway (Oct 03 2022 at 10:46):

From: Gerwin Klein <kleing@unsw.edu.au>
The AFP is now also forked at a74db29363f5: https://foss.heptapod.net/isa-afp/afp-2022

New entries will still go into afp-2021 for now, and commits to devel will appear in the release after Isabelle2022.

For any urgent changes for afp-2022, please send me email as announced.

Cheers,
Gerwin

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

Email Gateway (Oct 06 2022 at 12:42):

From: Makarius <makarius@sketis.net>
OK. See now https://isabelle.sketis.net/repos/isabelle-release/rev/7eedccabbc74

Makarius

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

Email Gateway (Oct 06 2022 at 12:43):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

Is there anything to say about it in NEWS?

Not that sure about it. But since the matter incited significant
discussion, here it is:

--

• HOL-Library.Signed_Division: class signed_division carries
  assumptions; use syntactic type classes signed_division and
  signed_modulo alternatively.

--

Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature

Last updated: Apr 26 2024 at 20:16 UTC