Hackage :: [Package]

hol: Higher order logic

[ library, logic, mit, program ] [ Propose Tags ]

This package implements a higher order logic kernel with OpenTheory support.

[Skip to Readme]

Modules

[Last Documentation]

  • HOL
    • HOL.Const
    • HOL.Data
    • HOL.Name
    • HOL.OpenTheory
    • HOL.Print
    • HOL.Rule
    • HOL.Sequent
    • HOL.Subst
    • HOL.Term
    • HOL.TermAlpha
    • HOL.TermData
    • HOL.Theory
    • HOL.Thm
    • HOL.Type
    • HOL.TypeData
    • HOL.TypeOp
    • HOL.TypeSubst
    • HOL.TypeVar
    • HOL.Var

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 1.0, 1.1, 1.2, 1.3, 1.4
Dependencies base (>=4.0 && <5.0), bytestring (>=0.9 && <0.10), containers (>=0.5 && <0.6), pretty (>=1.1 && <1.2), text (>=0.11 && <0.12), transformers (>=0.3 && <0.4) [details]
License MIT
Author Joe Leslie-Hurd <joe@gilith.com>
Maintainer Joe Leslie-Hurd <joe@gilith.com>
Category Logic
Source repo head: git clone git://github.com/gilith/hol.git
Uploaded by JoeHurd at 2017-08-24T22:12:15Z
Distributions NixOS:1.4
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 2684 total (18 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2017-08-24 [all 3 reports]

Readme for hol-1.1

[back to package description]

The hol package

The hol package is a Haskell library that implements a higher order logic kernel. It can read proof files in OpenTheory format, and includes a pretty-printer compatible with the standard theory library.

This software is released under the MIT License.

Install

Installing the hol package requires cabal:

git clone https://github.com/gilith/hol.git
cd hol
cabal install

Test

Use cabal to run the test suite:

cabal test

Profile

Before starting, make sure the GHC system and the GHC text and transformers libraries are installed with profiling support. On a Debian system the following command installs them:

 apt-get install ghc-prof libghc-text-prof libghc-transformers-prof

Next use cabal to install the other dependent libraries with profiling support:

cabal sandbox init
cabal configure --enable-library-profiling --enable-profiling --enable-benchmarks
cabal install --only-dependencies --enable-library-profiling

Build the hol package library and benchmark program:

cabal configure --enable-library-profiling --enable-profiling --enable-benchmarks
cabal build

Use the opentheory tool to create a benchmark file:

 opentheory info --article -o base.art base

Then use cabal to run the benchmark:

cabal bench

The time and memory allocation profile of the program can be viewed in text format:

less hol-profile.prof

Alternatively the memory allocation profile can be viewed as a graph:

hp2ps -e8in -c hol-profile.hp
ps2pdf hol-profile.ps
xpdf hol-profile.pdf