Package Details: isabelle 2017-1

Git Clone URL: https://aur.archlinux.org/isabelle.git (read-only)
Package Base: isabelle
Description: 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.
Upstream URL: https://www.cl.cam.ac.uk/research/hvg/Isabelle/
Licenses: custom:BSD
Groups: science
Submitter: bitwave
Maintainer: badcasa
Last Packager: badcasa
Votes: 21
Popularity: 0.023444
First Submitted: 2014-06-07 09:32
Last Updated: 2017-10-10 20:01

Dependencies (4)

Required by (5)

Sources (2)

Latest Comments

snape3058 commented on 2017-01-10 10:13

Hi,
The source download link has been modified to http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1_app.tar.gz

As a consequence, the PKGBUILD should be modified on line 17.

With new version number of 2016_1, all modifications will be as follows:

diff --git a/PKGBUILD b/PKGBUILD
index 90a8986..37f3bd5 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,7 +1,7 @@
# Maintainer: bitwave <aur [at] oomlu [dot] de>
# Contributor: Fabian Ruch <bafain [At] gmail [dOT] com>
pkgname=isabelle
-pkgver=2016
+pkgver=2016_1
pkgrel=1
pkgdesc="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."
arch=('i686' 'x86_64')
@@ -14,11 +14,11 @@ if test "$CARCH" == x86_64; then
'lib32-gcc-libs: for improved performance of Poly/ML on x86_64 machines')
fi
optdepends=('texlive-core: document preparation')
-source=(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle${pkgver//_/-}_linux.tar.gz
+source=(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle${pkgver//_/-}_app.tar.gz
isabelle.desktop)
-md5sums=('d92c888eb61f7bd51917d5a79a0eb8c0'
+md5sums=('7fbfd0af7ac722e3f961951106887f8a'
'd33d0dd09e9105f4f043bd5e59458481')
-sha256sums=('64f5357f638220a855311a604eaf8fc4bb7e703b7cf3ea997723ace875c6014a'
+sha256sums=('b9ac02fc086c7242a2424839d4daf9d4d24e9360fe3368fe20598758ab7b2cf0'
'84b61a83692939ca9e08402f1c55a06e4ccac8941664435d20b0ef0ceed9f43a')

build() {

cloud-oak commented on 2016-12-22 15:38

Newest Version is 2016_1, this patch to the PKGBUILD makes it work:

diff --git a/PKGBUILD b/PKGBUILD
index 90a8986..2900a63 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,7 +1,7 @@
# Maintainer: bitwave <aur [at] oomlu [dot] de>
# Contributor: Fabian Ruch <bafain [At] gmail [dOT] com>
pkgname=isabelle
-pkgver=2016
+pkgver=2016_1
pkgrel=1
pkgdesc="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."
arch=('i686' 'x86_64')
@@ -16,9 +16,9 @@ fi
optdepends=('texlive-core: document preparation')
source=(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle${pkgver//_/-}_linux.tar.gz
isabelle.desktop)
-md5sums=('d92c888eb61f7bd51917d5a79a0eb8c0'
+md5sums=('7fbfd0af7ac722e3f961951106887f8a'
'd33d0dd09e9105f4f043bd5e59458481')
-sha256sums=('64f5357f638220a855311a604eaf8fc4bb7e703b7cf3ea997723ace875c6014a'
+sha256sums=('b9ac02fc086c7242a2424839d4daf9d4d24e9360fe3368fe20598758ab7b2cf0'
'84b61a83692939ca9e08402f1c55a06e4ccac8941664435d20b0ef0ceed9f43a')

build() {

andrewchen commented on 2015-07-25 10:13

Hi,
I noticed this package conflicts and provides isabelle. However, this package is called isabelle, so it doesn't make much sense to conflict and provide itself.
EDIT: now fixed

simonzack commented on 2015-07-17 23:08

@bitwave:

Many thanks! Can I recommend some small changes to the desktop file?

[Desktop Entry]
Type=Application
Name=Isabelle
Comment=HOL based theorem prover
Exec=/usr/bin/isabelle jedit
Icon=/opt/isabelle/lib/icons/isabelle.xpm
Terminal=false
Categories=Education;Science;Math;
X-Desktop-File-Install-Version=0.22

I've:
- removed the double quotes to Exec so it works
- changed the icon to match the one displayed in the isabelle jedit window, I think it differentiates between isabelle and jedit as a text editor too
- changed the categories to match that of sage (I'm not sure if they're used though, but since sage does it...)

bitwave commented on 2015-07-16 17:28

@simonzack: i moved the 32-bit libs into optdepends. the desktop icon is in development. the problem is, i have no gnome, etc. window environment.

simonzack commented on 2015-07-15 19:42

@bitwave:

I removed these lines while installing isabelle yesterday:

if test "$CARCH" == x86_64; then
depends+=('lib32-glibc' 'lib32-gcc-libs')
fi

and it can still prove things, so I suppose that means they could be optional? Some searching on the internet suggests that the 64 bit libraries use more memory but is about the same speed.

My install currently depends on: perl perl-libwww python2

Another suggestion: perhaps there could be a menu icon for isabelle-jedit, using a *.desktop file?

bitwave commented on 2015-07-15 08:35

@simonzack: good question. I have no idea. Can you specify which libraries you need?

simonzack commented on 2015-07-15 02:12

Are 32 bit libraries necessary? I haven't compiled by myself but on the website it states "32-bit C/C++ standard libraries on 64-bit Linux (optional, for improved performance of Poly/ML)".

bitwave commented on 2015-06-02 14:06

updated to version 2015

bitwave commented on 2014-09-15 12:29

updated to version 2014