From: Makarius <email@example.com>
Some "unproven" changesets about a mysterious "go" component have shown up in
Isabelle/c9fb5e7975c5 and Isabelle/8347ffa1f92c (by Lars Hupel).
Since the isabelle-dev mailing list is the official channel for Isabelle
development, Lars has now an opportunity to explain the purpose of it. Right
now it looks like an unfinished private experiment that has escaped into the
Concerning Isabelle components in general, there are some explanations in
Admin/components/PLATFORMS. Without proper multi-platform support, components
rarely make any sense. "Works for me on Linux" is not sufficient.
Moreover, we now have the de-facto quality standard to assemble components as
(semi)automated and repeatable process in Isabelle/Scala. See the many
existing tools "isabelle component_XYZ".
Since this is all a lot of work and requires great care, we have de-facto
converged to a situation where I am the main provider and maintainer of all
As a minimum there should be a proper discussion about the need and purpose of
a particular component. The decision to support a particular external project,
by inclusion in the Isabelle space, should never be taken lightly.
isabelle-dev mailing list
Last updated: Mar 04 2024 at 10:08 UTC