On May 15 at 21:40 +0200, Makarius wrote: > On Tue, 15 May 2012, Timothy Bourke wrote: > > >Otherwise, there are FreeBSD ports of Poly/ML and Isabelle (2009.2): > > http://www.freshports.org/lang/polyml > > http://www.freshports.org/math/isabelle > > > >The patches therein may be helpful in building Isabelle on OpenBSD; or > >the current maintainer may already know how to solve some BSD issues. > > > >The trickiest step is usually to get Poly/ML working. > > Here is the famous quote from the Isabelle download and installation page: > > Warning: Pre-packaged versions of Isabelle, Poly/ML, and Proof General > floating through the Net as deb, rpm, port etc. are usually incomplete > and outdated! > > With the following empiric proof for this general statement against > homegrown packages: > http://www.freebsd.org/cgi/cvsweb.cgi/ports/lang/polyml/Makefile?rev=1.14;content-type=text%2Fplain Agreed! Personally, I saw the light many months ago, switched to Linux, and now download my packages directly from the Isabelle site like a good proof assistant assistant ;-) In fact, your earlier sage advice about packaging was instrumental in my conversion. But for those yet to reach this point, source ports, despite their shortcomings, at least provide a starting point for getting things working. In my opinion, a reasonable compromise may be to port Poly/ML and to download the Isabelle source directly. Tim.
Description: Digital signature