From 8470c438dd3b29ec368fb48601ab673c24748c38 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 2 Sep 2023 11:17:39 +0200 Subject: [PATCH] Add CoqEAL 2.0.0 --- .../packages/coq-coqeal/coq-coqeal.2.0.0/opam | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 released/packages/coq-coqeal/coq-coqeal.2.0.0/opam diff --git a/released/packages/coq-coqeal/coq-coqeal.2.0.0/opam b/released/packages/coq-coqeal/coq-coqeal.2.0.0/opam new file mode 100644 index 000000000..1ec4d6471 --- /dev/null +++ b/released/packages/coq-coqeal/coq-coqeal.2.0.0/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +maintainer: "Cyril Cohen " + +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 including normal forms of matrices, + 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.16" & < "8.19~") | (= "dev")} + "coq-bignums" + "coq-paramcoq" {>= "1.1.3"} + "coq-hierarchy-builder" {>= "1.4.0"} + "coq-mathcomp-ssreflect" {>= "2.0"} + "coq-mathcomp-algebra" + "coq-mathcomp-multinomials" {>= "2.0"} + "coq-mathcomp-real-closed" {>= "2.0"} +] + +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" + "Érik Martin-Dorel" + "Anders Mörtberg" + "Damien Rouhling" + "Pierre Roux" + "Vincent Siles" +] + +url { + src: "https://github.com/coq-community/coqeal/archive/refs/tags/2.0.0.tar.gz" + checksum: "sha512=8cc232e9704d99a48463a0909aaa5469acdd8e7587b11e2b5bee6a662c8ba51c2b4712e6ac9c3800dd22ae08767cb9039cc508cc10f88b7e0f13ed8047a80260" +}