blob: c94d88d0922eaa2bd41cc3f93955c20e6e96ac2e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
# Maintainer: Mort Yao <soi@mort.ninja>
# Contributor: Nikolaos Bezirgiannis <bezeria@gmail.com>
# FIXME: holyhammer fails to build with ocaml-num
pkgname=hol
pkgver=kananaskis.12
pkgrel=3
pkgdesc='HOL4 theorem-proving system'
url='https://hol-theorem-prover.org/'
arch=('x86_64')
license=('BSD')
install="$pkgname.install"
source=("http://sourceforge.net/projects/hol/files/hol/${pkgver//./-}/hol-${pkgver//./-}.tar.gz"
#
)
md5sums=('5b01d43494c7809c029764a95bf06402')
depends=('polyml' 'graphviz')
provides=('hol')
conflicts=('hol-git')
build() {
cd "${srcdir}/${pkgname}-${pkgver//./-}"
poly < tools/smart-configure.sml
bin/build
bin/build cleanForReloc
}
package() {
_oldtop="${srcdir}/${pkgname}-${pkgver//./-}"
_newtop="/opt/hol"
cd $_oldtop
# install everything under /opt/hol
install -m755 -d "${pkgdir}/opt/${pkgname}"
cp -r . "${pkgdir}/opt/${pkgname}"
# install license
install -m755 -d "${pkgdir}/usr/share/licenses/${pkgname}"
install -m644 COPYRIGHT "${pkgdir}/usr/share/licenses/${pkgname}/"
# make symlinks to /usr/bin
mkdir -p ${pkgdir}/usr/bin
ln -s /opt/hol/bin/hol ${pkgdir}/usr/bin/hol
ln -s /opt/hol/bin/hol.noquote ${pkgdir}/usr/bin/hol.noquote
ln -s /opt/hol/bin/Holmake ${pkgdir}/usr/bin/Holmake
}
|