diff options
| author | Nikolaos Bezirgiannis | 2015-07-06 23:11:34 +0200 |
|---|---|---|
| committer | Nikolaos Bezirgiannis | 2015-07-06 23:11:34 +0200 |
| commit | c0abf61ba35ca621c1c43bb99c8ec1073d3571fe (patch) | |
| tree | b4784c1c767ed851cfa9cdcfa24d28fc274bfe79 | |
| parent | c24c2692e5eed83b9f9e12fa0952ef665462235e (diff) | |
| download | aur-c0abf61ba35ca621c1c43bb99c8ec1073d3571fe.tar.gz | |
Fixed emitML for hol version 10
| -rw-r--r-- | .SRCINFO | 5 | ||||
| -rw-r--r-- | 0002-fix-emit.patch | 11 | ||||
| -rw-r--r-- | PKGBUILD | 13 |
3 files changed, 23 insertions, 6 deletions
@@ -1,19 +1,20 @@ pkgbase = hol pkgdesc = Interactive proof assistant for higher order logic pkgver = kananaskis.10 - pkgrel = 1 + pkgrel = 2 url = http://hol.sourceforge.net/ arch = i686 arch = x86_64 license = BSD depends = polyml - optdepends = graphviz conflicts = mesa-demos conflicts = hol-git source = http://sourceforge.net/projects/hol/files/hol/kananaskis-10/hol-kananaskis-10.tar.gz source = 0001-fix-holdir.patch + source = 0002-fix-emit.patch md5sums = aaf565484d62f1b43423897a2e8517ac md5sums = d613c3d825d6f382a24533c0136c5b1e + md5sums = 4a01da11b5bfb917a3e5a08ee8bde856 pkgname = hol diff --git a/0002-fix-emit.patch b/0002-fix-emit.patch new file mode 100644 index 000000000000..dbb472b827d4 --- /dev/null +++ b/0002-fix-emit.patch @@ -0,0 +1,11 @@ +--- a/src/emit/EmitML.sml 2015-07-06 22:38:46.266485633 +0200 ++++ b/src/emit/EmitML.sml 2015-07-06 22:39:00.063152051 +0200 +@@ -1532,7 +1532,7 @@ + fun emit_xML (Ocaml,sigSuffix,structSuffix) p (s,elems_0) = + let val _ = emitOcaml := Ocaml + val (pcs,elems) = internalize elems_0 (* pcs = pseudo-constrs *) +- val path = if p="" then FileSys.getDir() else p ++ val path = Path.concat(FileSys.getDir(), "ML/") + val pathPrefix = Path.concat(path, capitalize s) + val sigfile = pathPrefix^ sigSuffix + val structfile = pathPrefix^ structSuffix @@ -1,23 +1,26 @@ # Maintainer: Nikolaos Bezirgiannis <bezeria@gmail.com> pkgname=hol pkgver=kananaskis.10 -pkgrel=1 +pkgrel=2 pkgdesc="Interactive proof assistant for higher order logic" url='http://hol.sourceforge.net/' arch=('i686' 'x86_64') license=('BSD') source=("http://sourceforge.net/projects/hol/files/hol/${pkgver//./-}/hol-${pkgver//./-}.tar.gz" '0001-fix-holdir.patch' + '0002-fix-emit.patch' ) depends=('polyml') -optdepends=('graphviz') +#optdepends=('graphviz') conflicts=('mesa-demos' 'hol-git') md5sums=('aaf565484d62f1b43423897a2e8517ac' - 'd613c3d825d6f382a24533c0136c5b1e') + 'd613c3d825d6f382a24533c0136c5b1e' + '4a01da11b5bfb917a3e5a08ee8bde856') prepare() { cd "${srcdir}/${pkgname}-${pkgver//./-}" patch -p1 -i "${srcdir}/0001-fix-holdir.patch" + patch -p1 -i "${srcdir}/0002-fix-emit.patch" } build() { @@ -25,7 +28,7 @@ build() { #echo "val mosmldir = \"/usr/bin\";" > config-override echo "val holdir = \"/opt/hol\"" > tools-poly/poly-includes.ML poly < tools/smart-configure.sml - bin/build + bin/build -nograph } package() { @@ -51,6 +54,8 @@ package() { cp -r sigobj "${pkgdir}/opt/${pkgname}" cp -r bin "${pkgdir}/opt/${pkgname}" cp -r tools "${pkgdir}/opt/${pkgname}" + cp -r tools-poly "${pkgdir}/opt/${pkgname}" + cp -r help "${pkgdir}/opt/${pkgname}" # install license install -m755 -d "${pkgdir}/usr/share/licenses/${pkgname}" |