Re: [isabelle] Isabelle on OpenBSD?



On May 14 at 14:56 +0000, Aaron W. Hsu wrote:
> On Sun, 13 May 2012 13:30:03 +0200, Makarius wrote:
> > On Sun, 13 May 2012, Aaron W. Hsu wrote:
> > 
> >> Has anyone previously made an attempt to port or support the Isabelle
> >> Theorem prover on *BSD, particularly OpenBSD?
> > 
> > Last year I've seen a BSD user in France, and he actually managed to run
> > Isabelle after installing the Linux binary compatibility package for it.
> > The script lib/isabelle-platform already takes care of it in the sense
> > that any *BSD will be coerced into x86-linux.  You will also have to
> > install GNU bash.
> 
> Ah, I see, yes, on OpenBSD I use AMD64, which does not have support for 
> Linux compatibility. Thank you for the report. 

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.

Tim.

Attachment: signature.asc
Description: Digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.