How to Install and Uninstall hol-light Package on Ubuntu 22.04 LTS (Jammy Jellyfish)

Last updated: May 07,2024

Deprecated! Installation of this package may no longer be supported.

You can also install and uninstall the hol-light on the following distributions in the same way, as they are all based on the Ubuntu system

Kubuntu 22.04 LTS
Lubuntu 22.04 LTS
Xubuntu 22.04 LTS
Ubuntu MATE 22.04 LTS
Ubuntu Studio 22.04 LTS
Pop!_OS 22.04 LTS
Zorin OS 16 / Zorin OS 17
Ubuntu Budgie 22.04

1. Install "hol-light" package

Please follow the steps below to install hol-light on Ubuntu 22.04 LTS (Jammy Jellyfish)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                hol-light
            
                    
    
    Copied

2. Uninstall "hol-light" package

Here is a brief guide to show you how to uninstall hol-light on Ubuntu 22.04 LTS (Jammy Jellyfish):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                hol-light
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the hol-light package on Ubuntu 22.04 LTS (Jammy Jellyfish)

Package: hol-light
Architecture: amd64
Version: 20190729-4build5
Priority: optional
Section: universe/math
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 37630
Depends: camlp5, camlp5-y7l77, ocaml-nox-4.11.1
Suggests: readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev, python
Filename: pool/universe/h/hol-light/hol-light_20190729-4build5_amd64.deb
Size: 4835508
MD5sum: cea3b154a82fa260377f1ca217afb235
SHA1: d0166d8237e6b3e04971922e1e7cc4dde23e5580
SHA256: 2fcd8a794f7559afcafffb5a6d08e83e3688f8bfc2cceb70d760b7fac3366daf
SHA512: 06b0d5d859df6d3690bded4f77dcaa56389fe17744b4f662427aa8094cfcd8125782b701cb89afa3ab422200683a869c3396a42b509b2a1262258e28996af897
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Description-en: 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.
Description-md5: 4a69d13e99a5d21da7555a1ffc45abd5