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

[I] Stdlib for the Rocq Prover

[T] The standard library for the Rocq Prover provides components for both
[T] theorem proving and efficient verified programming.
[T]
[T] Provided functionality includes: arithmetic theorems and tactics, theorems
[T] for classical logic, algebra, real numbers, and efficient implementation of
[T] data types, for example, lists, sets, integer and floating-point numbers.

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

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

[C] extra/scientific

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

makeopt= # There is a Makefile but it completely ignores install paths
makeinstopt=
# Note: Exclude documentation for the time being, as T2 does not have
# sphinx_rtd_theme
hook_add postmake 5 "dune build --display=verbose -p rocq-stdlib"
hook_add postmake 5 "dune install --display=verbose -p rocq-stdlib --prefix=$root/$prefix --libdir=$root$libdir/site-lib"
export OCAMLPATH=$root$libdir/site-lib

[D] 469e90effc0f537ced5cd2cc8467b6f90cbc75849f6abe8741e3513c stdlib-9.0.0.tar.gz https://github.com/rocq-prover/stdlib/releases/download/V9.0.0/