coq

Proof assistant for higher-order logic
https://coq.inria.fr/

Current versions
8.7.1
HEAD

coq requires the following formulae to be installed:
ocaml-findlib 1.7.3 OCaml library manager
camlp5 7.03_1 Preprocessor and pretty-printer for OCaml
ocaml 4.06.0 General purpose programming language in the ML family
ocaml-num 1.1_1 OCaml legacy Num library for arbitrary-precision arithmetic

Reverse dependencies

The following formula requires coq to be installed:
compcert 3.2 Formally verified C compiler

Recent formula history

ilovezfs coq 8.7.1
ilovezfs coq: depend on ocaml-num
ilovezfs Use “squiggly” heredocs.
ilovezfs coq 8.7.0
Tej Chajed coq: expand test to include a plugin (#16940)

Formula code at GitHub