Package Details: isabelle 2025-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: gilcu3
Last Packager: gilcu3
Votes: 26
Popularity: 0.000889
First Submitted: 2014-06-07 09:32 (UTC)
Last Updated: 2025-03-25 13:54 (UTC)

Dependencies (5)

Required by (5)

Sources (2)

Latest Comments

« First ‹ Previous 1 2 3 Next › Last »

Jesko commented on 2019-06-11 18:01 (UTC) (edited on 2019-06-11 18:18 (UTC) by Jesko)

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 (UTC)

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() {

khdlr commented on 2016-12-22 15:38 (UTC) (edited on 2016-12-22 15:45 (UTC) by khdlr)

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 (UTC) (edited on 2016-03-02 05:04 (UTC) by andrewchen)

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 (UTC)

@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 (UTC)

@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 (UTC)

@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 (UTC)

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

simonzack commented on 2015-07-15 02:12 (UTC)

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 (UTC)

updated to version 2015

« First ‹ Previous 1 2 3 Next › Last »