Source: hol-light
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
 Hendrik Tews <hendrik@askra.de>
Build-Depends:
 debhelper-compat (= 12),
 camlp5 (>= 7.11),
 ocaml-base-nox,
 libnum-ocaml-dev,
 dh-ocaml
Standards-Version: 4.4.1
Rules-Requires-Root: no
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: https://salsa.debian.org/ocaml-team/hol-light.git
Vcs-Browser: https://salsa.debian.org/ocaml-team/hol-light

Package: hol-light
Architecture: any
Depends:
 camlp5,
 ${ocaml:Depends},
 ${shlibs:Depends},
 ${misc:Depends}
Suggests:
 readline-editor,
 prover9,
 coinor-csdp,
 pari-gp,
 maxima,
 dmtcp,
 libocamlgraph-ocaml-dev,
 python
Description: HOL Light theorem prover
 HOL Light is an interactive theorem prover for Higher-Order Logic
 with a very simple logical core running in an OCaml toplevel. HOL
 Light is famous for the verification of floating-point
 arithmetic as well as for the Flyspeck project, which aimed at the
 formalization of Tom Hales' proof of the Kepler conjecture.