Searches without login should now work. You must get asked to click a button.
Port details
isabelleGeneric proof assistant
2009.2mathΣ=0 2009.2Version of this port present on the latest quarterly branch.
BROKEN: Build seems to hang on the package builders DEPRECATED: Broken for more than 6 months This port expired on: 2015-02-28 IGNORE: is marked as broken: Build seems to hang on the package builders
There is no maintainer for this port.
Any concerns regarding this port should be directed to the FreeBSD Ports mailing list via ports@FreeBSD.org
Isabelle is a generic proof assistant. It allows mathematical
formulas to be expressed in a formal language and provides tools
for proving those formulas in a logical calculus. The main application
is the formalization of mathematical proofs and in particular formal
verification, which includes proving the correctness of computer
hardware or software and proving properties of computer languages
and protocols.
Compared with similar tools, Isabelle's distinguishing feature is
its flexibility. Most proof assistants are built around a single
formal calculus, typically higher-order logic. Isabelle has the
capacity to accept a variety of formal calculi. The distributed
version supports higher-order logic but also axiomatic set theory
and several other formalisms. See logics for more details.
Isabelle is a joint project between Lawrence C. Paulson (University
of Cambridge, UK) and Tobias Nipkow (Technical University of Munich,
Germany).
WWW: http://isabelle.in.tum.de
===> The following configuration options are available for isabelle-2009.2:
EMACS_PKG=off: Build with Emacs Packages
HOL_ALGEBRA=off: Build optional heap: HOL-Algebra
HOL_HOL4=off: Build optional heap: HOL4
HOL_NOMINAL=off: Build optional heap: HOL-Nominal
HOL_NSA=off: Build optional heap: HOL-NSA
HOL_TLA=off: Build optional heap: TLA
HOL_WORD=off: Build optional heap: HOL-Word
LEDIT=off: Use ledit as line editor
POLYML=off: Use Poly/ML (fast but broken) instead of SML/NJ
RLWRAP=on: Use rlwrap as line editor
===> Use 'make config' to modify these settings
[MAINTAINER] math/isabelle: update from 2007 to 2008
Updates the port to the latest Isabelle release. It does
not seem worth the effort to continually patch the bash
script files to make them work under sh, hence the large
number of removed files.
PR: ports/126067
Submitted by: Timothy Bourke <timbob@bigpond.com>
Bump portrevision due to upgrade of devel/gettext.
The affected ports are the ones with gettext as a run-dependency
according to ports/INDEX-7 (5007 of them) and the ones with USE_GETTEXT
in Makefile (29 of them).
PR: ports/124340
Submitted by: edwin@
Approved by: portmgr (pav)
Move the USE_PERL definitions, and others, before pre.mk inclusion. This
will be needed to conditionalize bsd.perl.mk inclusion.
Approved by: maintainer
Update port: math/isabelle
Update to Isabelle port:
* Works with updated sml-nj-devel port.
* Does not require bash
Thanks to Johannes 5 Joemann for helpful comments/patches.
PR: ports/116046
Submitted by: Timothy Bourke <timbob@bigpond.com>
math/isabelle does not build on pointyhat, because the build process
requires a non-standard kernel setting. Mark it as NO_PACKAGE.
Refer to http://docs.freebsd.org/cgi/mid.cgi?20060521015932.GB603
PR: ports/101749
Submitted by: Timothy Bourke <timbob at bigpond.com> (maintainer)
