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
public repository.
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
components.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
