How to Install and Uninstall coq Package on Kali Linux

Last updated: December 28,2024

1. Install "coq" package

Please follow the steps below to install coq on Kali Linux


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq
            
                    
    
    Copied

2. Uninstall "coq" package

This tutorial shows how to uninstall coq on Kali Linux:


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq package on Kali Linux

Package: coq
Version: 8.18.0+dfsg-1
Installed-Size: 304414
Maintainer: Debian OCaml Maintainers
Architecture: amd64
Replaces: coq-libs (<< 8.2.pl1)
Provides: coq-8.18.0+4.14.1
Depends: libcoq-stdlib (= 8.18.0+dfsg-1), libcoq-core-ocaml-fg9y1, libfindlib-ocaml-449z9, libstdlib-ocaml-ep7y0, libzarith-ocaml-zlfv4, ocaml-base-4.14.1, python3:any, libc6 (>= 2.35), libgmp10 (>= 2:6.3.0+dfsg), ocaml, ocaml-findlib
Suggests: coqide | proofgeneral, ledit | readline-editor, libcoq-core-ocaml-dev, why (>= 2.19), coq-doc
Breaks: coq-libs (<< 8.2.pl1)
Size: 81718924
SHA256: 3522fa87acc88c0ea49d2cf5245ed0c893f4a444d55c7396a913090ee55da483
SHA1: cb3799daf8a63c8359d976031e707658f1aec39e
MD5sum: bc438a122e7de2eaebebc092d8d436ec
Description: 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:
Homepage: http://coq.inria.fr/
Tag: devel::compiler, field::mathematics, implemented-in::ocaml,
interface::commandline, interface::text-mode, role::program,
scope::utility, uitoolkit::ncurses
Section: math
Priority: optional
Filename: pool/main/c/coq/coq_8.18.0+dfsg-1_amd64.deb