Package Details: hol kananaskis.10-3

Git Clone URL: https://aur.archlinux.org/hol.git (read-only)
Package Base: hol
Description: Interactive proof assistant for higher order logic
Upstream URL: http://hol.sourceforge.net/
Licenses: BSD
Conflicts: hol-git
Submitter: victor.vde
Maintainer: bezirg
Last Packager: bezirg
Votes: 3
Popularity: 0.220037
First Submitted: 2010-03-10 01:13
Last Updated: 2015-10-06 22:12

Dependencies (1)

Required by (0)

Sources (3)

Latest Comments

bezirg commented on 2014-09-29 08:19

xrcz: I answered you also at the github issue:

In Archlinux,

before I build, I patch src/prekernel/Globals.sml with

-val HOLDIR = Systeml.HOLDIR
+val HOLDIR = "/opt/hol"

I use mosml (it is slower than polyml, but polyml has conflicts problem in Archlinux with mesa-demos package)
and set the path of mosml in config-override.

> echo "val mosmldir = \"/usr/bin\";" > config-override

Then I build

> mosml < tools/smart-configure.sml
> bin/build

The smart configure will pick the build directory for SystemL directory. But for Globals.HOLDIR
the path is fixed to /opt/hol

After a succesful build, I have to package HOL:

1. I fixed all the broken symlinks under sigobj:

> for _link in $(find ${_oldtop}/sigobj/ -type l)
> do
> _oldsrc=$(readlink -v $_link)
> ln -sfn ${_oldsrc/$_oldtop/$_newtop} $_link
> done

I fix the dir references inside some text/script files to point to the install dir:

> sed -i -e 's,'"$_oldtop"','"$_newtop"',g' bin/hol bin/hol.bare bin/hol.bare.noquote bin/hol.noquote sigobj/SRCFILES

The package will install hol under /opt/hol/
and create symlinks of some hol bin programs to /usr/bin/

I tested hol for simple programs: open a theory, use some tactic, and it seems to work fine.

If you have any suggestion or you think this fix is incomplete, let me know.

xrchz commented on 2014-09-28 16:07

By the way, how would you say you have got around this issue?
https://github.com/HOL-Theorem-Prover/HOL/issues/105

bezirg commented on 2014-09-26 10:07

Fixed HOLDIR path issue.

bezirg commented on 2014-08-25 14:12

In other words, hol can successfully build with polyml, but currently arch is not polyml-friendly.

bezirg commented on 2014-08-25 14:09

Yes, but the decision to switch to mosml is mostly a pragmatic one.
People who have the extra/mesa-demos package already installed, cannot aur install neither polyml nor polyml-svn, since of a name conflict "/usr/bin/poly". Check also the discussion at the polyml aur page.

When (and if) the problem is resolved, I will be glad to switch it back to polyml. Another possible way is to build a hol-specialized polyml with the name conflict resolved, patch hol and then build hol.

xrchz commented on 2014-08-25 13:38

mosml is _much_ slower than polyml; if you can get this package working with polyml at all the hol developers would be keen to know (write to the hol-info mailing list). if you need some patch to the polyml-svn package comment on it.

bezirg commented on 2014-08-25 13:29

Moved from polyml to mosml, because a file in polyml package interferes with the package extra/mesa-demos

bezirg commented on 2014-08-20 14:28

Updated to latest stable release. Please, check also hol-git for the development version.

xrchz commented on 2012-09-19 21:18

kananaskis 8 is about to be released. this package needs an update.

incubos commented on 2011-01-11 15:25

The package needs root privileges to be built.