Package Details: isabelle 2023-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: bitwave
Last Packager: bitwave
Votes: 25
Popularity: 0.000002
First Submitted: 2014-06-07 09:32 (UTC)
Last Updated: 2023-09-18 11:16 (UTC)

Dependencies (3)

Required by (4)

Sources (2)

Latest Comments

1 2 Next › Last »

thestr4ng3r commented on 2020-07-04 08:37 (UTC)

The name of this package should be "isabelle-bin", as stated in https://wiki.archlinux.org/index.php/AUR_submission_guidelines#Rules_of_submission "Packages that use prebuilt deliverables, when the sources are available, must use the -bin suffix."

MW360 commented on 2020-06-11 12:50 (UTC)

Until the maintainer updates the PKGBUILD you can update it yourself with the following checksums or just use my package: isabelle-tum.

md5sums=('7c69d3aa39116cd4a91ad1592a0431e1' '63add57fc05e5334ad1582d07a0c7146')

brettgilio commented on 2020-03-27 18:07 (UTC)

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 (UTC) (edited on 2020-03-07 12:29 (UTC) by simonzack)

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

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

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

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

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

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