Edit Package ocaml-coq

Formal proof management system

https://opam.ocaml.org/packages/coq

The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g., the CompCert compiler certification project and the Bedrock verified low-level programming library), the formalization of mathematics (e.g., the full formalization of the Feit-Thompson theorem and homotopy type theory) and teaching.

Refresh
Refresh
Source Files
Filename Size Changed
_service 0000000701 701 Bytes 28 days
ocaml-coq-8.13.2.tar.xz 0005179424 4.94 MB 28 days
ocaml-coq.changes 0000000142 142 Bytes 28 days
ocaml-coq.patch 0000000452 452 Bytes about 1 month
ocaml-coq.spec 0000002956 2.89 KB 28 days
Comments for ocaml-coq 1

Bernd Singer's avatar

Tomcat42 wrote about 1 month ago

i had problems using it to build compcert. Ist seems, /usr/lib64/ocaml/coqc is not the default. Running "coqc" on the command line fails until the environament variable COQLIB is set correctly. I will try to set up a patch.

openSUSE Build Service is sponsored by