How to Install and Uninstall coq Package on Ubuntu 20.10 (Groovy Gorilla)

Last updated: December 24,2024

1. Install "coq" package

This tutorial shows how to install coq on Ubuntu 20.10 (Groovy Gorilla)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq
            
                    
    
    Copied

2. Uninstall "coq" package

Learn how to uninstall coq on Ubuntu 20.10 (Groovy Gorilla):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq package on Ubuntu 20.10 (Groovy Gorilla)

Package: coq
Architecture: amd64
Version: 8.12.0-3build1
Priority: optional
Section: universe/math
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 325233
Provides: coq-8.12.0+4.08.1
Depends: coq-theories (= 8.12.0-3build1), libcoq-ocaml-xtzl0, libnum-ocaml-f5qg6, ocaml-base-nox-4.08.1, python3:any, libc6 (>= 2.32), ocaml-nox, ocaml-findlib
Suggests: coqide | proofgeneral, ledit | readline-editor, libcoq-ocaml-dev, why (>= 2.19), coq-doc
Breaks: coq-libs (<< 8.2.pl1)
Replaces: coq-libs (<< 8.2.pl1)
Filename: pool/universe/c/coq/coq_8.12.0-3build1_amd64.deb
Size: 78727692
MD5sum: 345cb229db3027abac82315f21c81ac7
SHA1: 5fbcc12fc4967f0184fc870ee47cb7423b16888b
SHA256: 333fc6b7d9d71dee3b06b1f23cb81db4d6fc03f7f9b80f050ccafaab191735e4
SHA512: 3392d700f0cda818ed8173f45a091d23037c43bef374df2fdb3704762bc3b5ac56e7c82dc8f39f031e7ab7bb927b379a08ce6e903129d89cdba6642de198ec48
Homepage: http://coq.inria.fr/
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