hol kananaskis.12-2

5 files changed, 40 insertions, 74 deletions

diff --git a/.SRCINFO b/.SRCINFO
index cac72f94a69c..a5cc5b158b18 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,21 +1,18 @@
 # Generated by mksrcinfo v8
-# Tue Feb 26 16:45:59 UTC 2019
+# Fri Mar  1 01:27:39 UTC 2019
 pkgbase = hol
-	pkgdesc = Interactive proof assistant for higher order logic
+	pkgdesc = HOL4 theorem-proving system
 	pkgver = kananaskis.12
-	pkgrel = 1
-	url = http://hol.sourceforge.net/
-	arch = i686
+	pkgrel = 2
+	url = https://hol-theorem-prover.org/
+	install = hol.install
 	arch = x86_64
 	license = BSD
-	depends = mosml
-	conflicts = hol-git
+	depends = polyml
+	depends = graphviz
+	conflicts = ocaml-num
 	source = http://sourceforge.net/projects/hol/files/hol/kananaskis-12/hol-kananaskis-12.tar.gz
-	source = 0001-fix-holdir.patch
-	source = 0002-fix-emit.patch
 	md5sums = 5b01d43494c7809c029764a95bf06402
-	md5sums = d613c3d825d6f382a24533c0136c5b1e
-	md5sums = 4a01da11b5bfb917a3e5a08ee8bde856
 
 pkgname = hol
 
diff --git a/0001-fix-holdir.patch b/0001-fix-holdir.patch
deleted file mode 100644
index 3fbe6a09c27a..000000000000
--- a/0001-fix-holdir.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- a/src/prekernel/Globals.sml	2014-09-26 11:42:11.653305179 +0200
-+++ b/src/prekernel/Globals.sml	2014-09-26 11:42:50.039971664 +0200
-@@ -15,7 +15,7 @@
-  * Installation-specific information.                                        *
-  *---------------------------------------------------------------------------*)
- 
--val HOLDIR = Systeml.HOLDIR
-+val HOLDIR = "/opt/hol"
- 
- (*---------------------------------------------------------------------------*
-  * Version information                                                       *
diff --git a/0002-fix-emit.patch b/0002-fix-emit.patch
deleted file mode 100644
index dbb472b827d4..000000000000
--- a/0002-fix-emit.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- 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
diff --git a/PKGBUILD b/PKGBUILD
index 68b518d115fb..ac664d170c0b 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,35 +1,28 @@
 # Maintainer: Mort Yao <soi@mort.ninja>
 # Contributor: Nikolaos Bezirgiannis <bezeria@gmail.com>
+
 pkgname=hol
 pkgver=kananaskis.12
-pkgrel=1
-pkgdesc="Interactive proof assistant for higher order logic"
-url='http://hol.sourceforge.net/'
-arch=('i686' 'x86_64')
+pkgrel=2
+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"
-        '0001-fix-holdir.patch'
-        '0002-fix-emit.patch'
-    )
-md5sums=('5b01d43494c7809c029764a95bf06402'
-         'd613c3d825d6f382a24533c0136c5b1e'
-         '4a01da11b5bfb917a3e5a08ee8bde856')
-depends=('mosml')
-#optdepends=('graphviz')
-conflicts=('hol-git')
-
-prepare() {
-   cd "${srcdir}/${pkgname}-${pkgver//./-}"
-   patch -p1 -i "${srcdir}/0001-fix-holdir.patch"
-   patch -p1 -i "${srcdir}/0002-fix-emit.patch"
-   #echo "val holdir = \"/opt/hol\";" > tools-poly/poly-includes.ML
-   echo "val mosmldir = \"/usr/bin\";" > config-override
-}
+        #
+       )
+md5sums=('5b01d43494c7809c029764a95bf06402')
+depends=('polyml' 'graphviz')
+conflicts=('ocaml-num')
 
 build() {
   cd "${srcdir}/${pkgname}-${pkgver//./-}"
-  mosml < tools/smart-configure.sml
-  bin/build --nograph
+
+  poly < tools/smart-configure.sml
+  bin/build
+
+  bin/build cleanForReloc
 }
 
 package() {
@@ -38,24 +31,9 @@ package() {
 
   cd $_oldtop
 
-  # fix broken symlinks
-  for _link in $(find ${_oldtop}/sigobj/ -type l)
-  do
-    _oldsrc=$(readlink -v $_link)
-    ln -sfn ${_oldsrc/$_oldtop/$_newtop} $_link
-  done
-
-  # fix references inside text files
-  sed -i -e 's,'"$_oldtop"','"$_newtop"',g' bin/hol bin/hol.bare bin/hol.bare.noquote bin/hol.noquote sigobj/SRCFILES
-
-  # install hol programs and libraries under /opt/hol
+  # install everything under /opt/hol
   install -m755 -d "${pkgdir}/opt/${pkgname}"
-  install -m644 std.prelude "${pkgdir}/opt/${pkgname}"
-  cp -r src "${pkgdir}/opt/${pkgname}"
-  cp -r sigobj "${pkgdir}/opt/${pkgname}"
-  cp -r bin "${pkgdir}/opt/${pkgname}"
-  cp -r tools "${pkgdir}/opt/${pkgname}"
-  cp -r help "${pkgdir}/opt/${pkgname}"
+  cp -r . "${pkgdir}/opt/${pkgname}"
 
   # install license
   install -m755 -d "${pkgdir}/usr/share/licenses/${pkgname}"
@@ -66,5 +44,4 @@ package() {
   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
-
 }
diff --git a/hol.install b/hol.install
new file mode 100644
index 000000000000..7c3bd698a968
--- /dev/null
+++ b/hol.install
@@ -0,0 +1,14 @@
+# See also:
+# https://github.com/HOL-Theorem-Prover/HOL/commit/c2615dd
+
+post_install() {
+    cd /opt/hol
+    poly < tools/smart-configure.sml
+    bin/build --relocbuild
+}
+
+post_upgrade() {
+    cd /opt/hol
+    poly < tools/smart-configure.sml
+    bin/build --relocbuild
+}