diff --git a/opam/opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam b/opam/opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam new file mode 100644 index 0000000000..32691de0a8 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam @@ -0,0 +1,47 @@ +opam-version: "2.0" +synopsis: "Relation Algebra and KAT in Coq" +name: "coq-relation-algebra" +maintainer: "Damien Pous " +#TO SET BEFORE RELEASE +version: "dev" +homepage: "http://perso.ens-lyon.fr/damien.pous/ra/" +dev-repo: "git+https://github.com/damien-pous/relation-algebra.git" +bug-reports: "https://github.com/damien-pous/relation-algebra/issues" +license: "LGPL-3.0-or-later" +depends: [ + "ocaml" +#TO SET BEFORE RELEASE + "coq" {>= "8.18"} +# "coq" {>= "8.16" & < "8.17~"} +#TO REMOVE BEFORE RELEASE (TO MAKE THEM OPTIONAL) + "coq-mathcomp-ssreflect" + "coq-aac-tactics" +] +#TO SET BEFORE RELEASE +# depopts: [ "coq-mathcomp-ssreflect" "coq-aac-tactics" ] +build: [ + ["sh" "-exc" "./configure --%{coq-mathcomp-ssreflect:enable}%-ssr --%{coq-aac-tactics:enable}%-aac"] + [make "-j%{jobs}%"] +] +install: [make "install"] +tags: [ + "keyword:relation algebra" + "keyword:kleene algebra with tests" + "keyword:kat" + "keyword:allegories" + "keyword:residuated structures" + "keyword:automata" + "keyword:regular expressions" + "keyword:matrices" + "category:Mathematics/Algebra" + "logpath:RelationAlgebra" ] +authors: [ + "Damien Pous " + "Christian Doczkal " +] + +url { + src: "https://github.com/damien-pous/relation-algebra/archive/refs/tags/v1.7.10.tar.gz" + checksum: "sha512=9dd7601db9f25753709d4708ab878782580a7d3a858c0188948a10ea51fcbceddee86e5c42e7ddba2a53f65fcb4ee379b33e9c0996cdcef32b7b419d62e6e04e" +} + diff --git a/package_picks/package-pick-8.18+beta1.sh b/package_picks/package-pick-8.18+beta1.sh index c857d2fa69..78f5bc0956 100644 --- a/package_picks/package-pick-8.18+beta1.sh +++ b/package_picks/package-pick-8.18+beta1.sh @@ -142,7 +142,7 @@ then # General mathematics (which requires one of the above tools) # PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.6.5" # requires coq-mathcomp-solvable < "1.18~" PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.1" - #PACKAGES="${PACKAGES} coq-relation-algebra.1.7.9" # does not build even after relaxing version constraints + PACKAGES="${PACKAGES} coq-relation-algebra.1.7.10" # Formal languages, compilers and code verification PACKAGES="${PACKAGES} coq-reglang.1.2.0"