On Wed, 3 Apr 2013, Alexander Krauss wrote:
Thanks Alex, it always helps if someone else with substantial experience
explains things, so that I am not the lone voice in the desert. I let
your nice explanations stand as is.
The area of your issue (interaction with the underlying ML system) is
maintained by Makarius pretty much exclusively.
Just one concrete note here: it is David Matthews working here with me for
many years, to make it work very smoothly with Poly/ML while keeping
SML/NJ and older versions of Poly/ML on board somehow. I started myself
with ML pretty printing already in 1993, and can't say that will ever be
finished. In the mid-1990-ies there were certain gross shortcomings that
were even officially documented.
Note that when I venture myself to propose actual "patches" to Poly/ML,
the first thing David usually does is to turn the idea behind it in a
proper implementation in the sense of his code base, where he is the
proven expert. I am glad that he does take the time, and not just apply
the proposed patch and thus endanger the system integrity.
Also note that when I "improved" myself exception printing just some
months before the Isabelle2013, I messed up SML/NJ in a subtle way that
was not immediately visible. As a consequence some software archeologists
who try to reactivate Isabelle2013 in the distant future will have
problems working with it practically, because ML errors just produce
"exception Option raised".
So a change can never be a "fix". It is just some entropy on the code
base. Special efforts and attention is required to keep a positive
balance in the end.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
