How to Install and Uninstall coq Package on Ubuntu 23.10 (Mantic Minotaur)

Last updated: December 24,2024

1. Install "coq" package

Please follow the guidance below to install coq on Ubuntu 23.10 (Mantic Minotaur)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq
            
                    
    
    Copied

2. Uninstall "coq" package

Please follow the guidance below to uninstall coq on Ubuntu 23.10 (Mantic Minotaur):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq package on Ubuntu 23.10 (Mantic Minotaur)

Package: coq
Architecture: amd64
Version: 8.17.0+dfsg-1build1
Priority: optional
Section: universe/math
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 294239
Provides: coq-8.17.0+4.13.1
Depends: libcoq-stdlib (= 8.17.0+dfsg-1build1), libcoq-core-ocaml-2qnm1, libfindlib-ocaml-0thr1, libzarith-ocaml-ai549, ocaml-base-4.13.1, python3:any, libc6 (>= 2.35), libgmp10 (>= 2:6.2.1+dfsg1), ocaml-nox, ocaml-findlib
Suggests: coqide | proofgeneral, ledit | readline-editor, libcoq-core-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.17.0+dfsg-1build1_amd64.deb
Size: 93056978
MD5sum: ec3f567f4e89772648d742c9308b7be0
SHA1: 84558802030a6c2491d6aa45fcdae20301eabab5
SHA256: cc42a3d2099ecc011cacd3abec22a6ec505ab4fea28811f375125587471b7918
SHA512: 42888b279496c9315d2742435e801084f0617c925b410b9dc1f686a7e6db18458a72b70ede0835eb0a446e0be2d5a57ba943eb1eeefb2eb6c6cab908cdda2c5c
Homepage: http://coq.inria.fr/
Description: proof assistant for higher-order logic (toplevel and compiler)
Description-md5: 2c4259e8b83c839ff539d48b854ee31a