# --- T2-COPYRIGHT-BEGIN ---
# t2/package/*/rocq/rocq.desc
# Copyright (C) 2025 The T2 SDE Project
# SPDX-License-Identifier: GPL-2.0
# --- T2-COPYRIGHT-END ---

[I] Interactive theorem prover

[T] The Rocq Prover is an interactive theorem prover, or proof assistant.
[T] This means that it is designed to develop mathematical proofs,
[T] and especially to write formal specifications: programs and proofs that
[T] programs comply to their specifications.
[T]
[T] An interesting additional feature of Rocq is that it can automatically
[T] extract executable programs from specifications, as either OCaml or
[T] Haskell source code.

[U] https://rocq-prover.org/

[A] INRIA
[M] Tomas Glozar <tglozar@gmail.com>

[C] extra/scientific

[L] LGPL
[S] Stable
[V] 9.0.0
[P] X -----5---9 510.000

var_append makeopt ' ' dunestrap
confopt="-prefix $root/$prefix -libdir $root$libdir/site-lib/coq"
cleanconfopt=0
makeinstopt=
hook_add postmake 5 "dune build --display=verbose -p rocq-runtime,coq-core,rocq-core,coqide-server"
hook_add postmake 5 "dune install --display=verbose --prefix=$root/$prefix --libdir=$root$libdir/site-lib rocq-runtime coq-core rocq-core coqide-server"
export OCAMLPATH=$root$libdir/site-lib

[D] 336d742d303cc9599e953e2a757f93e24a34bfb2d59b200974e8fc84 rocq-9.0.0.tar.gz https://github.com/rocq-prover/rocq/releases/download/V9.0.0/