I have been working on emerging the 2016 versions of isabelle. Here is a working ebuild for version 2016, I am working on an ebuild for 2016-1 but that will require some work. Reproducible: Always
Created attachment 456520 [details] ebuild based on isabelle-2015
Created attachment 456522 [details, diff] classpath patch updated
Created attachment 456524 [details, diff] freechart classpath updated
Created attachment 456526 [details, diff] libsha1 patch updated
I added a dependency on z3, tested with the ebuild from the haskell overlay. I also dropped a patch that fixed issues with swi-prolog because my tests with swi-prolog 6.6 worked fine.
Thank you for your contribution. I could not open the URL is this the expected content? http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1/doc/NEWS.html In the ebuild I suggest to bump to EAPI=6, If possible, add a source, where upstream says so and which texlive version is required (we still have only texlive-2015): " #upstream says #bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, #for document preparation: complete LaTeX "
(In reply to Jonas Stein from comment #6) > Thank you for your contribution. > > I could not open the URL is this the expected content? > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1/doc/NEWS. > html Sorry, their website is changing at the same time I am working on these ebuilds so I linked to the wrong page. I corrected the URL field. > In the ebuild I suggest to bump to EAPI=6, I upgraded to EAPI 6, and change get_libdir to get_abi_LIBDIR since that sounds like the closest available option and I couldn't find any documentation about deprecating get_libdir. > If possible, add a source, where upstream says so and which texlive version > is required (we still have only texlive-2015): > " > #upstream says > #bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, > #for document preparation: complete LaTeX > " I couldn't find where upstream specifies those dependencies, so I am inclined to think this was a personal communication between the maintainer at that time and the Isabelle community.
Created attachment 456868 [details] ebuild based on isabelle-2015
(In reply to David E. Narváez from comment #8) > Created attachment 456868 [details] > ebuild based on isabelle-2015 Neat, thanks! I'll test it out and add to portage.
(In reply to Mark Wright from comment #9) > Neat, thanks! I'll test it out and add to portage. I am working on some changes right now that I need to test first, so if you could hold off your testings for a day or two until I post my latest version of the ebuild that would be great. Thanks!
Created attachment 457604 [details, diff] isabelle-2016.1-libsha1.patch
Created attachment 457606 [details] isabelle-2016.1.ebuild (In reply to David E. Narváez from comment #10) > (In reply to Mark Wright from comment #9) > > Neat, thanks! I'll test it out and add to portage. > > I am working on some changes right now that I need to test first, so if you > could hold off your testings for a day or two until I post my latest version > of the ebuild that would be great. Thanks! Thanks, I started hacking 2016.1 based on your work. This is a work in progress ebuild, it starts building, it will probably fail. Or if it builds, there will probably be problems at runtime. I'll add polyml-5.6 to portage soon. I will add sci-mathematics/z3 with isabelle support to portage later, which is why I removed the z3 stuff from the isabelle ebuild. I'm gienah in #gentoo-science on irc freenode if you'd like to discuss it there.
Oh, it wants z3 during the isabelle 2016-1 build: HOL-Word-SMT_Examples FAILED (see also /var/tmp/portage/sci-mathematics/isabelle-2016.1/work/Isabelle2016-1/heaps/polyml-5.6_X86_64-linux/log/HOL-Word-SMT_Examples) *** The SMT solver "z3" is not installed *** At command "by" (line 237 of "~~/src/HOL/SMT_Examples/SMT_Tests.thy") *** The SMT solver "z3" is not install So I'm putting your z3 stuff back.
Bumped, thanks for the help: commit 08c4c3f235caed7161be8696b7019064e20a4378 Author: Mark Wright <gienah@gentoo.org> Date: Tue Jan 3 09:47:13 2017 +1100 sci-mathematics/isabelle: Bump to 2016.1. Thanks to David E. Narv?ez for providing the isabelle 2016 patches and the 2016 ebuild. Thanks to mgorny for reporting the get_libdir called in global scope QA bug. Gentoo-bugs: 602958, 593380
