Debian 13 (Trixie) native package

hol-light

HOL Light theorem prover

Packages / Debian 13 (Trixie) / math / hol-light

[Source: hol-light]

Package: hol-light (1:3.0.0-2+b7)

Maintainers:

Debian OCaml Maintainers

External Resources:

Homepage: [www.cl.cam.ac.uk]

HOL Light theorem prover

Other Packages Related to hol-light:

dep: [camlp5]
Pre Processor Pretty Printer for OCaml - classical version
dep: camlp5-4new7
Package not available
dep: libcamlp-streams-ocaml-dev-0lin0
Package not available
dep: libcompiler-libs-ocaml-dev-4b6d0
Package not available
dep: libstdlib-ocaml-dev-m4xw9
Package not available
dep: libzarith-ocaml-dev-h79v1
Package not available
dep: ocaml-5.3.0
Package not available

sug: readline-editor
Package not available
sug: prover9
Package not available
sug: [coinor-csdp]
Software package for semidefinite programming (binaries)
sug: [pari-gp]
PARI/GP Computer Algebra System binaries
sug: [maxima]
Computer algebra system -- base system
sug: dmtcp
Package not available
sug: [libocamlgraph-ocaml-dev]
graph library for OCaml
sug: python
Package not available

Download hol-light

Architecture	Package Size	Installed Size	Files
amd64	5.7 MiB	45 MiB	[list of files]
arm64	5.7 MiB	45 MiB	[list of files]

Rutas de archivos del paquete (1,705)

Showing the first 250 sorted package-associated paths. Use file search to locate a specific path.

/usr/bin/hol-light
/usr/share/doc/hol-light/changelog.Debian.amd64.gz
/usr/share/doc/hol-light/changelog.Debian.arm64.gz
/usr/share/doc/hol-light/changelog.Debian.gz
/usr/share/doc/hol-light/changelog.gz
/usr/share/doc/hol-light/copyright
/usr/share/doc/hol-light/QUICK_REFERENCE.txt.gz
/usr/share/doc/hol-light/README.Debian
/usr/share/doc/hol-light/README.gz
/usr/share/doc/hol-light/VERYQUICK_REFERENCE.txt.gz
/usr/share/hol-light/100/arithmetic_geometric_mean.ml
/usr/share/hol-light/100/arithmetic.ml
/usr/share/hol-light/100/ballot.ml
/usr/share/hol-light/100/bernoulli.ml
/usr/share/hol-light/100/bertrand.ml
/usr/share/hol-light/100/birthday.ml
/usr/share/hol-light/100/cantor.ml
/usr/share/hol-light/100/cayley_hamilton.ml
/usr/share/hol-light/100/ceva.ml
/usr/share/hol-light/100/chords.ml
/usr/share/hol-light/100/circle.ml
/usr/share/hol-light/100/combinations.ml
/usr/share/hol-light/100/constructible.ml
/usr/share/hol-light/100/cosine.ml
/usr/share/hol-light/100/cubic.ml
/usr/share/hol-light/100/derangements.ml
/usr/share/hol-light/100/desargues.ml
/usr/share/hol-light/100/descartes.ml
/usr/share/hol-light/100/dirichlet.ml
/usr/share/hol-light/100/div3.ml
/usr/share/hol-light/100/divharmonic.ml
/usr/share/hol-light/100/e_is_transcendental.ml
/usr/share/hol-light/100/euler.ml
/usr/share/hol-light/100/feuerbach.ml
/usr/share/hol-light/100/fourier.ml
/usr/share/hol-light/100/four_squares.ml
/usr/share/hol-light/100/friendship.ml
/usr/share/hol-light/100/fta.ml
/usr/share/hol-light/100/gcd.ml
/usr/share/hol-light/100/heron.ml
/usr/share/hol-light/100/inclusion_exclusion.ml
/usr/share/hol-light/100/independence.ml
/usr/share/hol-light/100/isoperimetric.ml
/usr/share/hol-light/100/isosceles.ml
/usr/share/hol-light/100/konigsberg.ml
/usr/share/hol-light/100/lagrange.ml
/usr/share/hol-light/100/leibniz.ml
/usr/share/hol-light/100/lhopital.ml
/usr/share/hol-light/100/liouville.ml
/usr/share/hol-light/100/minkowski.ml
/usr/share/hol-light/100/morley.ml
/usr/share/hol-light/100/pascal.ml
/usr/share/hol-light/100/perfect.ml
/usr/share/hol-light/100/pick.ml
/usr/share/hol-light/100/piseries.ml
/usr/share/hol-light/100/platonic.ml
/usr/share/hol-light/100/pnt.ml
/usr/share/hol-light/100/polyhedron.ml
/usr/share/hol-light/100/primerecip.ml
/usr/share/hol-light/100/ptolemy.ml
/usr/share/hol-light/100/pythagoras.ml
/usr/share/hol-light/100/quartic.ml
/usr/share/hol-light/100/ramsey.ml
/usr/share/hol-light/100/ratcountable.ml
/usr/share/hol-light/100/realsuncountable.ml
/usr/share/hol-light/100/reciprocity.ml
/usr/share/hol-light/100/sqrt.ml
/usr/share/hol-light/100/stirling.ml
/usr/share/hol-light/100/subsequence.ml
/usr/share/hol-light/100/thales.ml
/usr/share/hol-light/100/triangular.ml
/usr/share/hol-light/100/two_squares.ml
/usr/share/hol-light/100/wilson.ml
/usr/share/hol-light/Arithmetic/arithprov.ml
/usr/share/hol-light/Arithmetic/definability.ml
/usr/share/hol-light/Arithmetic/derived.ml
/usr/share/hol-light/Arithmetic/fol.ml
/usr/share/hol-light/Arithmetic/godel.ml
/usr/share/hol-light/Arithmetic/make.ml
/usr/share/hol-light/Arithmetic/pa.ml
/usr/share/hol-light/Arithmetic/sigmacomplete.ml
/usr/share/hol-light/Arithmetic/tarski.ml
/usr/share/hol-light/arith.ml
/usr/share/hol-light/basics.ml
/usr/share/hol-light/bignum.cmi
/usr/share/hol-light/bignum.cmo
/usr/share/hol-light/bignum_num.ml
/usr/share/hol-light/bignum_zarith.ml
/usr/share/hol-light/bool.ml
/usr/share/hol-light/Boyer_Moore/boyer-moore.ml
/usr/share/hol-light/Boyer_Moore/clausal_form.ml
/usr/share/hol-light/Boyer_Moore/counterexample.ml
/usr/share/hol-light/Boyer_Moore/definitions.ml
/usr/share/hol-light/Boyer_Moore/environment.ml
/usr/share/hol-light/Boyer_Moore/equalities.ml
/usr/share/hol-light/Boyer_Moore/generalize.ml
/usr/share/hol-light/Boyer_Moore/induction.ml
/usr/share/hol-light/Boyer_Moore/irrelevance.ml
/usr/share/hol-light/Boyer_Moore/main.ml
/usr/share/hol-light/Boyer_Moore/make.ml
/usr/share/hol-light/Boyer_Moore/README
/usr/share/hol-light/Boyer_Moore/rewrite_rules.ml
/usr/share/hol-light/Boyer_Moore/shells.ml
/usr/share/hol-light/Boyer_Moore/struct_equal.ml
/usr/share/hol-light/Boyer_Moore/support.ml
/usr/share/hol-light/Boyer_Moore/terms_and_clauses.ml
/usr/share/hol-light/Boyer_Moore/testset/arith.ml
/usr/share/hol-light/Boyer_Moore/testset/list.ml
/usr/share/hol-light/Boyer_Moore/testset/res1.pdf
/usr/share/hol-light/Boyer_Moore/testset/res2.pdf
/usr/share/hol-light/Boyer_Moore/waterfall.ml
/usr/share/hol-light/Cadical/cadical.ml
/usr/share/hol-light/Cadical/cnf.ml
/usr/share/hol-light/Cadical/dimacs.ml
/usr/share/hol-light/Cadical/ldrup.ml
/usr/share/hol-light/Cadical/make.ml
/usr/share/hol-light/Cadical/README
/usr/share/hol-light/Cadical/test.ml
/usr/share/hol-light/calc_int.ml
/usr/share/hol-light/calc_num.ml
/usr/share/hol-light/calc_rat.ml
/usr/share/hol-light/canon.ml
/usr/share/hol-light/cart.ml
/usr/share/hol-light/class.ml
/usr/share/hol-light/Complex/complex_grobner.ml
/usr/share/hol-light/Complex/complexnumbers.ml
/usr/share/hol-light/Complex/complex_real.ml
/usr/share/hol-light/Complex/complex_transc.ml
/usr/share/hol-light/Complex/cpoly.ml
/usr/share/hol-light/Complex/fundamental.ml
/usr/share/hol-light/Complex/grobner_examples.ml
/usr/share/hol-light/Complex/make.ml
/usr/share/hol-light/Complex/quelim_examples.ml
/usr/share/hol-light/Complex/quelim.ml
/usr/share/hol-light/compute.ml
/usr/share/hol-light/database.ml
/usr/share/hol-light/define.ml
/usr/share/hol-light/Divstep/divstep_bounds.ml
/usr/share/hol-light/Divstep/divstep.ml
/usr/share/hol-light/Divstep/hull-light-20230416.sage
/usr/share/hol-light/Divstep/hull_light.ml
/usr/share/hol-light/Divstep/idivstep.ml
/usr/share/hol-light/Divstep/Makefile
/usr/share/hol-light/Divstep/make.ml
/usr/share/hol-light/Divstep/README
/usr/share/hol-light/doc-to-help.sed
/usr/share/hol-light/drule.ml
/usr/share/hol-light/EC/ccsm2.ml
/usr/share/hol-light/EC/computegroup.ml
/usr/share/hol-light/EC/curve25519.ml
/usr/share/hol-light/EC/edmont.ml
/usr/share/hol-light/EC/edwards25519.ml
/usr/share/hol-light/EC/edwards448.ml
/usr/share/hol-light/EC/edwards.ml
/usr/share/hol-light/EC/excluderoots.ml
/usr/share/hol-light/EC/exprojective.ml
/usr/share/hol-light/EC/family25519.ml
/usr/share/hol-light/EC/formulary_jacobian.ml
/usr/share/hol-light/EC/formulary_projective.ml
/usr/share/hol-light/EC/formulary_xzprojective.ml
/usr/share/hol-light/EC/jacobian.ml
/usr/share/hol-light/EC/make.ml
/usr/share/hol-light/EC/misc.ml
/usr/share/hol-light/EC/montgomery.ml
/usr/share/hol-light/EC/montwe.ml
/usr/share/hol-light/EC/nistp192.ml
/usr/share/hol-light/EC/nistp224.ml
/usr/share/hol-light/EC/nistp256.ml
/usr/share/hol-light/EC/nistp384.ml
/usr/share/hol-light/EC/nistp521.ml
/usr/share/hol-light/EC/projective.ml
/usr/share/hol-light/EC/README
/usr/share/hol-light/EC/secp192k1.ml
/usr/share/hol-light/EC/secp224k1.ml
/usr/share/hol-light/EC/secp256k1.ml
/usr/share/hol-light/EC/wei25519.ml
/usr/share/hol-light/EC/weierstrass.ml
/usr/share/hol-light/EC/x25519.ml
/usr/share/hol-light/EC/xzprojective.ml
/usr/share/hol-light/equal.ml
/usr/share/hol-light/Examples/bdd_examples.ml
/usr/share/hol-light/Examples/bitblast.ml
/usr/share/hol-light/Examples/bondy.ml
/usr/share/hol-light/Examples/borsuk.ml
/usr/share/hol-light/Examples/brunn_minkowski.ml
/usr/share/hol-light/Examples/combin.ml
/usr/share/hol-light/Examples/complexpolygon.ml
/usr/share/hol-light/Examples/cong.ml
/usr/share/hol-light/Examples/cooper.ml
/usr/share/hol-light/Examples/dickson.ml
/usr/share/hol-light/Examples/digit_serial_methods.ml
/usr/share/hol-light/Examples/division_algebras.ml
/usr/share/hol-light/Examples/dlo.ml
/usr/share/hol-light/Examples/forster.ml
/usr/share/hol-light/Examples/gcdrecurrence.ml
/usr/share/hol-light/Examples/harmonicsum.ml
/usr/share/hol-light/Examples/hol88.ml
/usr/share/hol-light/Examples/holby.ml
/usr/share/hol-light/Examples/inverse_bug_puzzle_miz3.ml
/usr/share/hol-light/Examples/inverse_bug_puzzle_tac.ml
/usr/share/hol-light/Examples/kb.ml
/usr/share/hol-light/Examples/lagrange_lemma.ml
/usr/share/hol-light/Examples/lucas_lehmer.ml
/usr/share/hol-light/Examples/machin.ml
/usr/share/hol-light/Examples/mangoldt.ml
/usr/share/hol-light/Examples/mccarthy.ml
/usr/share/hol-light/Examples/miller_rabin.ml
/usr/share/hol-light/Examples/misiurewicz.ml
/usr/share/hol-light/Examples/mizar.ml
/usr/share/hol-light/Examples/multiwf.ml
/usr/share/hol-light/Examples/padics.ml
/usr/share/hol-light/Examples/pell.ml
/usr/share/hol-light/Examples/polylog.ml
/usr/share/hol-light/Examples/prog.ml
/usr/share/hol-light/Examples/prover9.ml
/usr/share/hol-light/Examples/pseudoprime.ml
/usr/share/hol-light/Examples/rectypes.ml
/usr/share/hol-light/Examples/reduct.ml
/usr/share/hol-light/Examples/safetyliveness.ml
/usr/share/hol-light/Examples/schnirelmann.ml
/usr/share/hol-light/Examples/solovay.ml
/usr/share/hol-light/Examples/sos.ml
/usr/share/hol-light/Examples/ste.ml
/usr/share/hol-light/Examples/sylvester_gallai.ml
/usr/share/hol-light/Examples/update_database.ml
/usr/share/hol-light/Examples/vitali.ml
/usr/share/hol-light/Examples/zolotarev.ml
/usr/share/hol-light/firstorder.ml
/usr/share/hol-light/Formal_ineqs/arith/arith_cache.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_float.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_nat.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_num.hl
/usr/share/hol-light/Formal_ineqs/arith/eval_interval.hl
/usr/share/hol-light/Formal_ineqs/arith/float_pow.hl
/usr/share/hol-light/Formal_ineqs/arith/float_theory.hl
/usr/share/hol-light/Formal_ineqs/arith/interval_arith.hl
/usr/share/hol-light/Formal_ineqs/arith/more_float.hl
/usr/share/hol-light/Formal_ineqs/arith/num_exp_theory.hl
/usr/share/hol-light/Formal_ineqs/arith_options.hl
/usr/share/hol-light/Formal_ineqs/docs/FormalVerifier.pdf
/usr/share/hol-light/Formal_ineqs/docs/FormalVerifier.tex
/usr/share/hol-light/Formal_ineqs/examples_flyspeck.hl
/usr/share/hol-light/Formal_ineqs/examples.hl
/usr/share/hol-light/Formal_ineqs/examples_other.hl
/usr/share/hol-light/Formal_ineqs/examples_poly.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_asn_acs.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_atn.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_eval_interval.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_exp.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_float.hl

Field source: Debian 13 (Trixie) main amd64 revision trixie-main-amd64:3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3

Usar este paquete

OpenFactory puede arrancar este sistema operativo en una máquina virtual del navegador, o iniciar una construcción que incluye el nombre nativo del paquete de este registro.

Probar Debian 13 (Trixie) en el navegador Construir una imagen que incluye hol-light

Versiones, suites y repositorios

Cada fila es metadato del índice de paquetes para una versión, arquitectura, suite y repositorio. Nombres, URL y tamaños vienen de la fuente; un enlace es un punto de descarga que puede cambiar, no una redistribución de OpenFactory.

Version	Release	Architecture	Repository	Package size	Installed size	Publisher repository artifact
1:3.0.0-2+b7	trixie / main	amd64	Debian 13 · main · amd64	5.7 MiB	45 MiB	pool/main/h/hol-light/hol-light_3.0.0-2+b7_amd64.deb
1:3.0.0-2+b7	trixie / main	arm64	Debian 13 · main · arm64	5.7 MiB	45 MiB	pool/main/h/hol-light/hol-light_3.0.0-2+b7_arm64.deb

Field source: Debian 13 (Trixie) main amd64 revision trixie-main-amd64:3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3

Sumas de comprobación y fechas de observación

For an APT source, signature verification authenticates the repository metadata chain and the Packages index containing this source-reported artifact digest. It does not certify package safety.

1:3.0.0-2+b7 / amd64Observed Sep 1, 2026 to Sep 1, 2026

Verification status: Metadata observed; artifact bytes were not independently fetched or hashed by this catalog import. The digest below is source-reported.

Source-reported sha256: c5925927be57c9e4a3357b61d126af5bfa9a760beb743f5dcc611224993053b4

After downloading that exact artifact, compare its bytes with the source-reported expected digest:

printf '%s  %s\n' 'c5925927be57c9e4a3357b61d126af5bfa9a760beb743f5dcc611224993053b4' 'hol-light_3.0.0-2+b7_amd64.deb' | sha256sum --check --strict -

A match establishes equality with the repository metadata value. It does not establish safety or catalog-side artifact retrieval.

Field source: Debian 13 (Trixie) main amd64 revision trixie-main-amd64:3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3

1:3.0.0-2+b7 / arm64Observed Sep 1, 2026 to Sep 1, 2026

Verification status: Metadata observed; artifact bytes were not independently fetched or hashed by this catalog import. The digest below is source-reported.

Source-reported sha256: e0a927d6250b303d5b4f7342aa373b0960b39add6f03126d84483d31cdba04cc

After downloading that exact artifact, compare its bytes with the source-reported expected digest:

printf '%s  %s\n' 'e0a927d6250b303d5b4f7342aa373b0960b39add6f03126d84483d31cdba04cc' 'hol-light_3.0.0-2+b7_arm64.deb' | sha256sum --check --strict -

A match establishes equality with the repository metadata value. It does not establish safety or catalog-side artifact retrieval.

Field source: Debian 13 (Trixie) main arm64 revision trixie-main-arm64:753da751bbc7a679f48bd1b623ffd4479cb6861c426118284c76eb82909e4908

Completitud del registro

The completeness score measures metadata coverage, not software quality, security, compatibility, or suitability.

Summary and description: 25/25
Artifact path and source digest: 25/25
Dependency metadata: 15/15
Package-file index: 15/15
Homepage: 5/5
License text: 0/5
Source package or maintainer: 10/10

Recorded total: 95/100

Field source: Debian 13 (Trixie) main amd64 revision trixie-main-amd64:3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3, Debian 13 (Trixie) main arm64 revision trixie-main-arm64:753da751bbc7a679f48bd1b623ffd4479cb6861c426118284c76eb82909e4908. The cross-OS mapping is catalog-derived from the source-reported homepage; it does not establish authorship or publisher identity

Fuentes y procedencia

Field-source links above resolve here. Each source entry names the metadata publisher, trust tier, exact snapshot revision, signature result, and observation time; catalog-derived mappings are labeled separately.

Debian 13 (Trixie) main amd64Sep 1, 2026
Authoritative source; repository metadata signature verified, revision trixie-main-amd64:3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3
Signature verification covers the configured repository metadata chain. It does not certify that the package is safe or suitable.
Repository-signature verification record
Signed object
https://deb.debian.org/debian/dists/trixie/InRelease
Signed-object SHA-256
98b25b5cd185c59d34aa6e4c3e9b5b8f01bbe9d104fe2dcfbcd30dc0a14a59ed
Signer fingerprint
4CB50190207B4758A3F73A796ED0E7B82643E131
Keyring revision
debian-archive-keyring.gpg
SHA-256 506b815cbb32d9b6066b4a2aa524071e071761e7e7f68c3ac74f3061ba852017
Tool and policy
gpgv (GnuPG) 2.4.9
openfactory-software-catalog-signature-v1
Verification time
Sep 1, 2026
Signed Release → package-index hash linkage
Path: main/binary-amd64/Packages.xz
Expected SHA-256: 3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3
Observed SHA-256: 3ab4e811cf4f3e5a335d382c58cc19d85f1abe7a4ef4689160ca1f637fa0e9b3
Result: match verified
Debian 13 (Trixie) main arm64Sep 1, 2026
Authoritative source; repository metadata signature verified, revision trixie-main-arm64:753da751bbc7a679f48bd1b623ffd4479cb6861c426118284c76eb82909e4908
Signature verification covers the configured repository metadata chain. It does not certify that the package is safe or suitable.
Repository-signature verification record
Signed object
https://deb.debian.org/debian/dists/trixie/InRelease
Signed-object SHA-256
98b25b5cd185c59d34aa6e4c3e9b5b8f01bbe9d104fe2dcfbcd30dc0a14a59ed
Signer fingerprint
4CB50190207B4758A3F73A796ED0E7B82643E131
Keyring revision
debian-archive-keyring.gpg
SHA-256 506b815cbb32d9b6066b4a2aa524071e071761e7e7f68c3ac74f3061ba852017
Tool and policy
gpgv (GnuPG) 2.4.9
openfactory-software-catalog-signature-v1
Verification time
Sep 1, 2026
Signed Release → package-index hash linkage
Path: main/binary-arm64/Packages.xz
Expected SHA-256: 753da751bbc7a679f48bd1b623ffd4479cb6861c426118284c76eb82909e4908
Observed SHA-256: 753da751bbc7a679f48bd1b623ffd4479cb6861c426118284c76eb82909e4908
Result: match verified