blob: 632bd5097153d65ec2fa804d27549f58bd1807fb (
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.13
pkgrel=3
pkgdesc='HOL4 theorem-proving system'
url='https://hol-theorem-prover.org/'
arch=('x86_64')
license=('BSD')
install="$pkgname.install"
source=("https://github.com/HOL-Theorem-Prover/HOL/archive/${pkgver//./-}.tar.gz"
#
)
md5sums=('f40da5a4141739831441380646ca09e7')
depends=('polyml' 'graphviz')
provides=('hol')
conflicts=('hol-git')
build() {
cd "${srcdir}/HOL-${pkgver//./-}"
poly < tools/smart-configure.sml
bin/build
bin/build cleanForReloc
}
package() {
_oldtop="${srcdir}/HOL-${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
}
|