Email Gateway (Aug 18 2022 at 19:39): Email Gateway (Aug 18 2022 at 19:39):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Has anyone previously made an attempt to port or support the Isabelle
Theorem prover on *BSD, particularly OpenBSD?
Email Gateway (Aug 18 2022 at 19:39):From: Makarius <makarius@sketis.net>
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.
The JVM is another issue -- I have not tried nor seen it recently, but it
might work as well, once sufficiently many Linux shared libraries are
installed on BSD.
Makarius
Email Gateway (Aug 18 2022 at 19:40):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Ah, I see, yes, on OpenBSD I use AMD64, which does not have support for
Linux compatibility. Thank you for the report.
Email Gateway (Aug 18 2022 at 19:41):From: Timothy Bourke <tim@tbrk.org>
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.
signature.asc
Email Gateway (Aug 18 2022 at 19:42):From: Makarius <makarius@sketis.net>
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
The file was started in 2005, last updated in 2010, and the underlying
Poly/ML version seems to be 5.4.0, but the current stable one is 5.4.1. It
also seems to lack support for libgmp (nice to have) and libsha1 (quite
important).
This is just the bottom of the problem. All the add-ons components for
the full system integration of the Isabelle bundle are still missing, see
also http://isabelle.in.tum.de/website-Isabelle2012-RC2/dist/
Makarius
Email Gateway (Aug 18 2022 at 19:42):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Makarius wrote:
What would it take to get OpenBSD supported as one of the platforms? I am
not currently using it because I do not have some of the applications, such
as Isabelle that my current research requires, but I would like to move back
to OpenBSD if I could. I would be willing to work on the porting efforts if
someone could point me to some information on what is normally required to
build an Isabelle bundle.
Looking at Poly/ML, I note that it appears to want static address ranges for
a database, which, if I am reading correctly, could require some work, since
OpenBSD uses randomized memory allocation. On the other hand, so do many of
the Linux systems out there today, so I suspect that I am misunderstanding
some of the Poly/ML porting guidelines.
I will probably not start on a port right away, but if there is interest, I
will definitely add it to my list.
Email Gateway (Aug 18 2022 at 19:42):From: Timothy Bourke <tim@tbrk.org>
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.
signature.asc
Email Gateway (Aug 18 2022 at 19:42):From: Makarius <makarius@sketis.net>
This used to be the classic way until 2007 or 2008. Then more and more add-on
tools were made available by default. Isabelle2012 already approximates some
kind of operating system distribution for logic-based tools, with SPASS, E, Z3
etc.
I've also taken away the freedom to choose a JVM -- a particular version is
bundled by default. This investment of 150 MB extra disk space solves a lot of
problems of everybody. E.g. I've first had both Java 6 and Java 7 as an option
for Isabelle2012, but after some months a few dropouts in jEdit on Java 7
(update 4) were discovered, so it is back to the 1.6 now. For the next release
after Isabelle2012, another JVM will be taken on board, independently of any
other JVMs that might be installed elsewhere.
For Windows I also bundle a full Cygwin installation at merely 99 MB. That's a
real bargain compared to the logic image sizes:
HOL 32bit: 140 MB
HOL 64bit: 280 MB
That is the default heap environment that the user needs to download
(compressed) and unpack -- as part of the main bundle. It takes in the range
of minutes to do so.
Since the coming Poly/ML release is anticipated to be very fast in building HOL
and producing the image -- and when we've finally abolished the dependency of
"make" in the build process -- the logic images could be built on the spot
after download.
Makarius
Email Gateway (Aug 18 2022 at 19:42):From: David Matthews <dm@prolingua.co.uk>
Please ignore the old "Porting" document. I hadn't realised it was
still on the website. I'll get rid of it since Poly/ML has not used
static address ranges since version 5.0 many years ago.
It's very likely that the Poly/ML tar-ball will compile and install on
OpenBSD with at most some minor tweaks. I've just compiled the SVN
version on FreeBSD and just had to add an include file that it required.
David
Last updated: May 06 2024 at 12:29 UTC