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.
Description: Digital signature