On Tue, 25 Sep 2012, Mark Wright wrote:
Did you include the important libsha1.so that is part of the regular Isabelle2012 distribution of Poly/ML?
No, thanks for letting me know I should, I guess I should build it from the source code here:
This is one of the clones floating around. The actual sources used to build Poly/ML are shipped with our standard polyml-5.4.1 archive, or now the polyml-5.5.0 components http://isabelle.in.tum.de/components/polyml-5.5.0.tar.gz
All these Isabelle components have a README that explains how it was built, and how it can in principle be reconstructed independently, although that is a lot of redundant work.
I use Isabelle. I have added sci-mathematics/spass-3.7, sci-mathematics/e-1.6 and sci-mathematics/cvc3-2.4.1 to portage with isabelle use flags, that automatically create their settings files and add themselves to the isabelle components file.
I am prepared to fix issues and to add more Isabelle components to portage for those components that can be built from the source code.
An impressive amount of work just to make things conformant to Gentoo. You also seem to be exceptional in using the result yourself, unlike many Linux hobbyists who merely package things and let the world stumble on the problems of the result.
Nonetheless, you will always be one step behind the real Isabelle distribution. Next time we depend essentially on Java 7 with JavaFX from Oracle, and I can't say how far the OpenJDK version of that is.
In the end the main question is how to serve users best. There is hardly anybody missing a Debianized version of Isabelle, but people occasionally come to me and say I should bundle even more things in the one big Isabelle distribution, bypassing problems of their standard OS packages.
Makarius