# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 5.1.1 The OCaml compiler (virtual package)
ocaml-base-compiler 5.1.1 Official release 5.1.1
ocaml-config 3 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
homepage: "https://math-comp.github.io/"
bug-reports: "https://github.com/math-comp/math-comp/issues"
dev-repo: "git+https://github.com/math-comp/math-comp.git"
license: "CECILL-B"
build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/algebra" "install" ]
depends: [ "coq-mathcomp-fingroup" { = version } ]
tags: [
"keyword:small scale reflection"
"keyword:mathematical components"
"keyword:algebra"
"keyword:algebraic structure hierarchies"
"keyword:archimedean field"
"keyword:floor"
"keyword:ceil"
"keyword:intervals"
"keyword:matrices"
"keyword:vectors"
"keyword:block matrices"
"keyword:determinant"
"keyword:Cramer rule"
"keyword:Vandermonde matrices"
"keyword:LUP decomposition"
"keyword:Gaussian elimination"
"keyword:matrix rank"
"keyword:eigen values"
"keyword:single variable polynomials"
"keyword:bivariate polynomials"
"keyword:polynomial division"
"keyword:integers"
"keyword:rational numbers"
"keyword:semi rings"
"keyword:rings"
"keyword:left algebra"
"keyword:left module"
"keyword:unit rings"
"keyword:field"
"keyword:algebraically closed field"
"keyword:additive morphisms"
"keyword:ring morphisms"
"keyword:finite dimensional vector spaces"
"keyword:complex numbers"
"keyword:square root"
"logpath:mathcomp.algebra"
]
authors: [ "The Mathematical Components team" ]
synopsis: "Mathematical Components Library on Algebra"
description: """
This library contains definitions and theorems about discrete
(i.e. with decidable equality) algebraic structures : ring, fields,
ordered fields, real fields, modules, algebras, integers, rational
numbers, polynomials, matrices, vector spaces...
"""
url {
src: "https://github.com/math-comp/math-comp/archive/mathcomp-1.19.0.tar.gz"
checksum: "sha256=786db902d904347f2108ffceae15ba29037ff8e63a6c58b87928f08671456394"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-mathcomp-algebra.1.19.0 coq.8.18.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-mathcomp-algebra.1.19.0 coq.8.18.0opam list; echo; timeout 4h opam install -y -v coq-mathcomp-algebra.1.19.0 coq.8.18.0Total: 27 M
../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrnum.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/matrix.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/matrix.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrnum.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssralg.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxalgebra.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssralg.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polydiv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxalgebra.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/poly.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polydiv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/poly.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxpoly.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxpoly.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrint.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/interval.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/vector.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/vector.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/intdiv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/intdiv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrint.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/rat.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/interval.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/rat.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssralg.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrnum.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/finalg.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/fraction.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/finalg.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/qpoly.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ring_quotient.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/matrix.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polyXY.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polyXY.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxalgebra.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/fraction.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polydiv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/poly.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ring_quotient.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/countalg.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/countalg.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/zmodp.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/mxpoly.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/vector.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/zmodp.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/finalg.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ssrint.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/intdiv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/rat.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/interval.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/countalg.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/qpoly.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/ring_quotient.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/all_algebra.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/polyXY.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/zmodp.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/fraction.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/all_algebra.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/mathcomp/algebra/all_algebra.vopam remove -y coq-mathcomp-algebra.1.19.0