How to Install and Uninstall coq Package on Ubuntu 16.04 LTS (Xenial Xerus)

Last updated: December 27,2024

1. Install "coq" package

Please follow the steps below to install coq on Ubuntu 16.04 LTS (Xenial Xerus)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq
            
                    
    
    Copied

2. Uninstall "coq" package

Please follow the instructions below to uninstall coq on Ubuntu 16.04 LTS (Xenial Xerus):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq package on Ubuntu 16.04 LTS (Xenial Xerus)

Package: coq
Priority: optional
Section: universe/math
Installed-Size: 22623
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Architecture: amd64
Version: 8.4pl4dfsg-3build2
Replaces: coq-libs (<< 8.2.pl1)
Provides: coq-8.4pl4+4.02.3
Depends: coq-theories (= 8.4pl4dfsg-3build2), emacsen-common, libcoq-ocaml-d91z1, ocaml-base-nox-4.02.3, libc6 (>= 2.15)
Recommends: coqide | proofgeneral
Suggests: ocaml-nox, proofgeneral, ledit | readline-editor, libcoq-ocaml-dev, why (>= 2.19), coq-doc
Breaks: coq-libs (<< 8.2.pl1)
Filename: pool/universe/c/coq/coq_8.4pl4dfsg-3build2_amd64.deb
Size: 3993698
MD5sum: 4a4b65a58f7f81a6ef57859b5b9d3594
SHA1: e7c89f076d85d42479fcaf45e052a7772829a15d
SHA256: 8c94ac749ad3e271ce3064c153f74e22946623b6738ecc4310ff08a6f5d40971
Description-en: proof assistant for higher-order logic (toplevel and compiler)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp5.
.
This package provides coqtop, a command line interface to Coq.
.
A graphical interface for Coq is provided in the coqide package.
Coq can also be used with ProofGeneral, which allows proofs to be
edited using emacs and xemacs. This requires the proofgeneral
package to be installed.
Description-md5: 2c4259e8b83c839ff539d48b854ee31a
Homepage: http://coq.inria.fr/
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu