Makarius makarius@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