How to Install and Uninstall hol-light Package on Ubuntu 20.10 (Groovy Gorilla)

Last updated: April 29,2024

1. Install "hol-light" package

Please follow the guidance below to install hol-light on Ubuntu 20.10 (Groovy Gorilla)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                hol-light
            
                    
    
    Copied

2. Uninstall "hol-light" package

Please follow the steps below to uninstall hol-light on Ubuntu 20.10 (Groovy Gorilla):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                hol-light
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the hol-light package on Ubuntu 20.10 (Groovy Gorilla)

Package: hol-light
Architecture: amd64
Version: 20190729-4build3
Priority: optional
Section: universe/math
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 37557
Depends: camlp5, camlp5-zlsj0, ocaml-nox-4.08.1
Suggests: readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev, python
Filename: pool/universe/h/hol-light/hol-light_20190729-4build3_amd64.deb
Size: 4775076
MD5sum: 8ee91a8c5a228d828c43874a03755b7f
SHA1: e56c48adaee3dea0e1bbe368feda1b8c943cc227
SHA256: 806b835783d42cc7b088001fc121cf29681303758105839570fcf671ae853f15
SHA512: 010743fb69bfa865b915d093f326ff98cfca434a2aefe40c33bc6b122e62b005a71c49e62b30c76f18a99df593f6a02f985a17fb82e88e246bc4ccdf51d33598
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