We've got some updates regarding OBS and GitHub/GitLab integration. Have a look and let us know what you think! 🧐


Edit Package ocaml-coq

Formal proof management system


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.

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

Bernd Singer's avatar

Tomcat42 wrote 3 months 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