Package Details: isabelle 2024-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: 26
Popularity: 0.007539
First Submitted: 2014-06-07 09:32 (UTC)
Last Updated: 2024-06-23 11:38 (UTC)

Latest Comments

« First ‹ Previous 1 2

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

bitwave commented on 2014-09-15 12:29 (UTC)

updated to version 2014

« First ‹ Previous 1 2