Makarius <makar...@sketis.net> writes: > On Thu, 20 Sep 2012, Mark Wright wrote: > >> I bumped polyml to 5.5 in portage (as 5.5.0 since that is the version >> reported by poly -v). Isabelle 2012 built fine with polyml 5.5. > > Are you sure about this?
Hi Makarius, Proofs with proof-general and sledgehammer with e 1.6 and spass 3.7 work. The isabelle test suite returns a 0 exit status during the build. isabelle jedit works with a simple proof. > 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 > You probably know already that I am very sceptical about this packaging of > Isabelle components as "native" OS packages. In so many years I've never > seen a packaging that was right, and it is getting more and more difficult > to achieve that with all the Isabelle add-ons that are now standard. > > > Makarius The issues I know of: - No source code to spass 3.8ds or later available. I would very much like to provide a more recent release of spass. - Haskabelle does not compile with the current version of haskell-src-exts. Its on my todo list to ask the haskell-src-exts maintainers to consider adding the support for undefined pragmas. - I have an ebuild for z3 integration with sledgehammer. I may not add that to portage though as it is packaging a binary. Gentoo's open source philosophy is to build packages from the source code. 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. Thanks, Mark _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
