Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 75882 - ebuild request: HOL theorem proof assistant
Summary: ebuild request: HOL theorem proof assistant
Status: CONFIRMED
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: Current packages (show other bugs)
Hardware: All Linux
: Normal normal (vote)
Assignee: Default Assignee for New Packages
URL: https://hol-theorem-prover.org
Whiteboard:
Keywords:
Depends on:
Blocks:
 
Reported: 2004-12-27 23:28 UTC by Radu Grigore
Modified: 2017-05-30 07:07 UTC (History)
2 users (show)

See Also:
Package list:
Runtime testing required: ---


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Radu Grigore 2004-12-27 23:28:50 UTC
Would it be possible to include HOL in the gentoo distribution? AFAIK(!) it depends only on mosml (which is already included).

Reproducible: Always
Steps to Reproduce:
1.
2.
3.
Comment 1 James Earl Spahlinger 2009-07-15 16:47:59 UTC
Please note that there is now version 5 of this out. I am attempting to write an ebuild but I am having some problems getting the dependencies working correctly. Additionally I think this should be assigned to maintainer wanted. Once I get the ebuild working, I'll submit it.
Comment 2 Andreas K. Hüttel archtester gentoo-dev 2010-07-01 18:40:59 UTC
Latest release HOL4 (2009)
Comment 3 Jonas Stein gentoo-dev 2017-05-30 07:07:29 UTC
repository is now on github:
https://github.com/HOL-Theorem-Prover/HOL