Package Details: hol kananaskis.14-1

Git Clone URL: https://aur.archlinux.org/hol.git (read-only, click to copy)
Package Base: hol
Description: HOL4 theorem-proving system
Upstream URL: https://hol-theorem-prover.org/
Licenses: BSD
Conflicts: hol-git
Provides: hol
Submitter: victor.vde
Maintainer: soimort
Last Packager: soimort
Votes: 5
Popularity: 0.000000
First Submitted: 2010-03-10 01:13 (UTC)
Last Updated: 2021-02-07 21:05 (UTC)

Latest Comments

bezirg commented on 2014-09-29 08:19 (UTC)

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 (UTC)

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 (UTC)

Fixed HOLDIR path issue.

bezirg commented on 2014-08-25 14:12 (UTC)

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

bezirg commented on 2014-08-25 14:09 (UTC)

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 (UTC)

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 (UTC)

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 (UTC)

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

xrchz commented on 2012-09-19 21:18 (UTC)

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

incubos commented on 2011-01-11 15:25 (UTC)

The package needs root privileges to be built.