sci-mathematics / isabelle

Isabelle is a generic proof assistant

Official package sites : ·

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.

v2016.1 :: 0/2016.1 :: gentoo (Masked by set 3281)

~amd64 ~x86
USE flags
doc graphbrowsing ledit readline


Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
Generate theory browsing information, including HTML documents that show a theory's definition, the theorems proved in its ML file and the relationship with its ancestors and descendants.
Use ledit for the isabelle tty line editor
Use readline (rlwrap) for the isabelle tty line editor


ELIBC setting for systems that use the FreeBSD C library

app-misc / ledit : A line editor to be used with interactive commands

app-misc / rlwrap : GNU readline wrapper

app-shells / bash : The standard GNU Bourne again shell

dev-java / itext : Generate documents in the Portable Document Format (PDF) and/or HTML

dev-java / java-config : Java environment configuration query tool

dev-java / jcommon : A collection of useful classes used by JFreeChart, JFreeReport and others

dev-java / jfreechart : JFreeChart is a free Java class library for generating charts

dev-java / jortho : A Java spell-checking library

dev-java / xz-java : Implementation of xz data compression in pure java

dev-lang / ghc : The Glasgow Haskell Compiler

dev-lang / perl : Larry Wall's Practical Extraction and Report Language

dev-lang / polyml : Poly/ML is a full implementation of Standard ML

dev-lang / scala : The Scala Programming Language

dev-lang / swi-prolog : versatile implementation of the Prolog programming language

dev-tex / rail : Offers syntax/railroad diagrams

sci-libs / coinor-csdp : COIN-OR C Library for Semi-Definite Programming

sci-mathematics / z3 : An efficient theorem prover

virtual / jdk : Virtual for Java Development Kit (JDK)

virtual / latex-base : Virtual for basic LaTeX binaries

dev-java / java-config : Java environment configuration query tool

dev-perl / libwww-perl : A collection of Perl Modules for the WWW

sci-mathematics / sha1-polyml : implementation of SHA1 is taken from the GNU coreutils package

virtual / jre : Virtual for Java Runtime Environment (JRE)

sci-mathematics / cvc3 : CVC3 is a theorem prover for Satisfiability Modulo Theories (SMT) problems

sci-mathematics / e : E is a theorem prover for full first-order logic with equality

sci-mathematics / kodkodi : A text front-end for the Kodkod Java library

sci-mathematics / spass : An Automated Theorem Prover for First-Order Logic with Equality

sci-mathematics/isabelle: Fails to compile due to scala dependency issue

Aaron Bauman
sec bug #636976, unmaintained in Gentoo, license forked multiple times. Removal in 30 days.
  • app-text/jpdftweak
  • dev-java/itext
  • dev-util/deskzilla
  • media-sound/tuxguitar
  • sci-chemistry/jmol
  • sci-mathematics/cvc3
  • sci-mathematics/e
  • sci-mathematics/isabelle
  • sci-mathematics/kodkodi
  • sci-mathematics/spass
Repository mirror & CI · gentoo
Merge updates from master
Patrice Clement · gentoo
sci-mathematics/isabelle: fix scala dependency.
Signed-off-by: Patrice Clement <> Package-Manager: Portage-2.3.49, Repoman-2.3.11
Francesco Turco · gentoo
sci-mathematics/isabelle: use HTTPS for links to
Robin H. Johnson · gentoo
Drop $Id$ per council decision in bug #611234.
Signed-off-by: Robin H. Johnson <>
Mark Wright · gentoo
sci-mathematics/isabelle: Remove old
Package-Manager: portage-2.3.3
T. Malfatti · gentoo
media-libs/portaudio: Version bump
Mark Wright · gentoo
sci-mathematics/isabelle: Bump to 2016.1. Thanks to David E. Narv?ez for providing the isabelle 2016 patches and the 2016 ebuild. Thanks to mgorny for reporting the get_libdir called in global scope QA bug.
Gentoo-bugs: 602958, 593380 Package-Manager: portage-2.3.3
Ian Delaney · gentoo
Merge remote-tracking branch 'remotes/sbraz/syncthing'
Pull Request:
James Le Cuirot · gentoo
sci-mathematics/isabelle: Remove old
Package-Manager: portage-2.2.27
Mark Wright · gentoo
sci-mathematics/isabelle: Remove sci-mathematics/csdp, as found existing sci-libs/coinor-csdp
Package-Manager: portage-2.2.27
Mark Wright · gentoo
sci-mathematics/isabelle: Bump to 2015, check diskspace and memory.
Thanks to Toralf F?rster for reporting the need to check diskspace, and Jonas Jelten for requesting the version bump. Gentoo-Bugs: 548864 562864 Package-Manager: portage-2.2.27
Justin Lecher · gentoo
Use https by default
Convert all URLs for sites supporting encrypted connections from http to https Signed-off-by: Justin Lecher <>
Robin H. Johnson · gentoo
proj/gentoo: Initial commit
This commit represents a new era for Gentoo: Storing the gentoo-x86 tree in Git, as converted from CVS. This commit is the start of the NEW history. Any historical data is intended to be grafted onto this point. Creation process: 1. Take final CVS checkout snapshot 2. Remove ALL ChangeLog* files 3. Transform all Manifests to thin 4. Remove empty Manifests 5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$ 5.1. Do not touch files with -kb/-ko keyword flags. Signed-off-by: Robin H. Johnson <> X-Thanks: Alec Warner <> - did the GSoC 2006 migration tests X-Thanks: Robin H. Johnson <> - infra guy, herding this project X-Thanks: Nguyen Thai Ngoc Duy <> - Former Gentoo developer, wrote Git features for the migration X-Thanks: Brian Harring <> - wrote much python to improve cvs2svn X-Thanks: Rich Freeman <> - validation scripts X-Thanks: Patrick Lauer <> - Gentoo dev, running new 2014 work in migration X-Thanks: Michał Górny <> - scripts, QA, nagging X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed