[isabelle-dev] Are sources available?

[Alexander Krauss]

Dear Yuri,

Am 16.06.2019 um 20:31 schrieb Yuri:
> On 2019-06-16 11:20, Makarius wrote:
>>
>>
>> Considering to produce a BSD "port" of Isabelle just to run it as a
>> user is unrealistic, not to say insane. We don't have a mailing list
>> for insanities.

I agree with Lars's comment about the tone of the above, and (hoping to
speak for others in the Isabelle community) I want to apologize for how
this was said.

> It seems that you are implying that the Isabelle code is convoluted
> beyond imaginable. We probably don't want such code then, because it
> can't possibly be useful for any purpose in such condition anyway.

I totally understand your reaction.

Still, to give you some context, Isabelle's code base has been around
for more than 30 years. It has evolved from experimental research
software and is still exclusively developed by researchers, often as
part of their PhD thesis or similar work. Large parts of it are
developed in a language that has never had a large community and whose
compiler is now maintained by a single person. The system accumulated
complexity through the integration of many third-party tools (e.g.
various ATPs), a deep integration with the PolyML compiler and
substantial moving parts for the GUI integration. These third-party
tools ship with Isabelle in a way that mostly hides the integration
complexity from users but would make repackaging attempts very hard,
especially when done by people not intimately familiar with Isabelle.
This can even be harmful when the problematic packages appear in OS
distributions.

That said, I still find Isabelle useful.

Alex