# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.11.0 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
homepage: "https://github.com/coq-community/coqeal"
dev-repo: "git+https://github.com/coq-community/coqeal.git"
bug-reports: "https://github.com/coq-community/coqeal/issues"
license: "MIT"
synopsis: "CoqEAL - The Coq Effective Algebra Library"
description: """
This Coq library contains a subset of the work that was developed in the context
of the ForMath EU FP7 project (2009-2013). It has two parts:
- theory, which contains developments in algebra and optimized algorithms on mathcomp data structures.
- refinements, which is a framework to ease change of data representations during a proof."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.10" & < "8.15~"}
"coq-bignums"
"coq-paramcoq" {(>= "1.1.1") | (= "dev")}
"coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")}
"coq-mathcomp-algebra" {((>= "1.12.0" & < "1.14~") | = "dev")}
]
tags: [
"category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
"keyword:effective algebra"
"keyword:elementary divisor rings"
"keyword:Smith normal form"
"keyword:mathematical components"
"keyword:Bareiss"
"keyword:Karatsuba multiplication"
"keyword:refinements"
"logpath:CoqEAL"
]
authors: [
"Guillaume Cano"
"Cyril Cohen"
"Maxime Dénès"
"Anders Mörtberg"
"Damien Rouhling"
"Vincent Siles"
]
url {
src: "https://github.com/coq-community/coqeal/archive/refs/tags/1.0.6.tar.gz"
checksum: "sha512=537ef553580bfc8dc59a80ca0a882caf30b454ef559bddebe9ae4ba335e0a22858c8d31b13757cf579a52aa008b09e7211e5cae32417572b6b574751acd78566"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-coqeal.1.0.6 coq.8.11.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-coqeal.1.0.6 coq.8.11.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-coqeal.1.0.6 coq.8.11.0Total: 43 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/refinements.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/param.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/multipoly.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hpoly.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/bareiss_eff.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/kaplansky.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/dvdring.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/dvdring.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/kaplansky.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/multipoly.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hpoly.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqpoly.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/similar.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smithpid.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/polydvd.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/mxstructure.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/fpmod.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smith.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/polydvd.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/edr.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/coherent.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binint.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/stronglydiscrete.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binrat.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/stronglydiscrete.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/fpmod.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqpoly.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/binetcauchy.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/rational.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss_dvdring.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/mxstructure.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/similar.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/edr.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/coherent.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx_complements.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binrat.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssrcomplements.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binint.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_div.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/examples/irred.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/binetcauchy.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/minor.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smithpid.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/bareiss_eff.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/karatsuba.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/atomic_operations.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binnat.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smith.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/rational.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss_dvdring.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/toomcook.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binnat.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssrcomplements.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/gauss.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/multipoly.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/minor.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/rank.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/refinements.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/dvdring.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/strassen.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/examples/irred.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/karatsuba.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binord.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/karatsuba.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/atomic_operations.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx_complements.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_div.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_op.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/boolF2.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/trivial_seq.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hrel.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssralg_ring_tac.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/bareiss_eff.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/pos.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/toomcook.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/karatsuba.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hpoly.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/kaplansky.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/fpmod.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/polydvd.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/rank.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/strassen.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/gauss.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/stronglydiscrete.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqpoly.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/mxstructure.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binord.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binrat.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/similar.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/coherent.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/edr.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/binetcauchy.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binint.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/refinements.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binnat.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/rational.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/bareiss_dvdring.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smithpid.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hrel.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/smith.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/boolF2.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssrcomplements.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/trivial_seq.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/examples/irred.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/seqmx_complements.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/minor.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/atomic_operations.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/pos.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/param.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_div.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssralg_ring_tac.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/karatsuba.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_op.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/binord.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/strassen.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/toomcook.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/boolF2.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/rank.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/gauss.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/param.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/hrel.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/trivial_seq.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/karatsuba.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/pos.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/theory/ssralg_ring_tac.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/CoqEAL/refinements/poly_op.vopam remove -y coq-coqeal.1.0.6