[isabelle-dev] Status of Isabelle "go" component

[Makarius]

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