Re: [polyml] polyml 5.5 Test071.ML = Failed!!

2012-09-26 Thread Makarius

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:

https://bitbucket.org/makarius


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

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


Re: [polyml] polyml 5.5 Test071.ML = Failed!!

2012-09-26 Thread Ian Zimmerman

Makarius In the end the main question is how to serve users best.
Makarius There is hardly anybody missing a Debianized version of
Makarius Isabelle, but people occasionally come to me and say I should
Makarius bundle even more things in the one big Isabelle distribution,
Makarius bypassing problems of their standard OS packages.

Here is one datapoint the other way.  I wish Isabelle was DFSG free and
I wish it was possible to package it.  I will not use the binary bundle,
just as I will not use a binary bundle of, say, Adobe Reader, however
convenient it might seem at any given moment.

I would be interested to know what the problems of their standard OS
packages are, in the case of Debian.

-- 
Ian Zimmerman
gpg public key: 1024D/C6FF61AD
fingerprint: 66DC D68F 5C1B 4D71 2EE5  BD03 8A00 786C C6FF 61AD
http://www.gravatar.com/avatar/c66875cda51109f76c6312f4d4743d1e.png
Rule 420: All persons more than eight miles high to leave the court.
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml