Package Details: isabelle 2020-1

Git Clone URL: https://aur.archlinux.org/isabelle.git (read-only, click to copy)
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: 22
Popularity: 0.019562
First Submitted: 2014-06-07 09:32
Last Updated: 2020-04-18 21:39

Dependencies (3)

Required by (5)

Sources (2)

Latest Comments

1 2 Next › Last »

brettgilio commented on 2020-03-27 18:07

Building isabelle... ==> Making package: isabelle 2019-1 (Fri 27 Mar 2020 01:04:42 PM CDT) ==> Checking runtime dependencies... ==> Checking buildtime dependencies... ==> Retrieving sources... -> Found Isabelle2019_linux.tar.gz -> Found isabelle.desktop ==> Validating source files with md5sums... Isabelle2019_linux.tar.gz ... FAILED isabelle.desktop ... Passed ==> ERROR: One or more files did not pass the validity check! Failed to build isabelle

simonzack commented on 2020-03-07 12:27

Is this dependent on python 2? It appears that the only .py files are:

  • /opt/isabelle/contrib/polyml-5.8/src/libpolyml/libffi/generate-ios-source-and-headers.py
  • /opt/isabelle/contrib/polyml-5.8/src/libpolyml/libffi/generate-osx-source-and-headers.py

Mac isn't relevant to Arch Linux.

simonzack commented on 2020-01-05 06:55

I cannot find anywhere in the docs where this requires python 2. This is one of the few packages that still has it marked as a dependency, which might not be a dependency at all?

thestr4ng3r commented on 2019-10-27 08:25

Is python2 really required? It seems to work fine for me without having it installed.

Jesko commented on 2019-06-11 18:01

Hi, there is a new version of isabelle. I modified the pkgbuild. The year and name of the tar changed.

https://pastebin.com/7M1X48qT

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.