How to Install and Uninstall hol-light Package on Ubuntu 16.04 LTS (Xenial Xerus)

Last updated: May 07,2024

1. Install "hol-light" package

This guide let you learn how to install hol-light on Ubuntu 16.04 LTS (Xenial Xerus)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                hol-light
            
                    
    
    Copied

2. Uninstall "hol-light" package

This guide covers the steps necessary to uninstall hol-light on Ubuntu 16.04 LTS (Xenial Xerus):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                hol-light
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the hol-light package on Ubuntu 16.04 LTS (Xenial Xerus)

Package: hol-light
Priority: optional
Section: universe/math
Installed-Size: 21895
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Architecture: amd64
Version: 20131026-1build2
Depends: camlp5, camlp5-tli55, ocaml-nox-4.02.3
Suggests: readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev
Filename: pool/universe/h/hol-light/hol-light_20131026-1build2_amd64.deb
Size: 2887654
MD5sum: 5b8716c88cbefd984caef782357c65cc
SHA1: f4925c06772afbb164ddff045ae452746461f0fa
SHA256: 51fa547e4691de77867336cb4822a0721c354099355d7130773d8ce13abf2f30
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 aims at the
formalization of Tom Hales' proof of the Kepler conjecture.
Description-md5: dd99a4d17d1f2693631036e77802a382
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu