Merge pull request #3325 from quimFIB/coq-formalv-1.3.0

coq-formalv release 1.3.0

released/packages/coq-formalv-check_range/coq-formalv-check_range.1.3.0/opam

@@ -0,0 +1,48 @@
+opam-version: "2.0"
+synopsis: "Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables" # One-line description
+description: """
+FV Check Range provides tactics to automatically prove Boolean goals
+involving 1, 2 or 3 Uint63.int/Sint63.int bounded variables through
+brute-force computation.
+""" # Longer description, can span several lines
+
+homepage: "https://gitlab.com/formalv/formalv"
+dev-repo: "git+https://gitlab.com/formalv/formalv"
+bug-reports: "https://gitlab.com/formalv/formalv/-/issues"
+doc: "https://formalv.gitlab.io/formalv/coqdoc/toc.html"
+maintainer: "Mireia González Bedmar <[email protected]>"
+
+tags: [
+  "keyword:automation"
+  "keyword:primitive integers"
+  "logpath:formalv.check_range"
+]
+
+authors: [
+  "Ana de Almeida Borges"
+  "Quim Casals Buñuel"
+  "Juan Conejero Rodriguez"
+  "Mireia González Bedmar"
+  "Eduardo Hermo Reyes"
+]
+
+license: "PolyForm Noncommercial License 1.0.0" # Make sure this is reflected by a LICENSE file in your sources
+
+depends: [
+  "coq" {>= "8.19" & < "8.20~"}
+  "coq-mathcomp-algebra" {>= "2.3" & < "2.4~" }
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4~" }
+  "coq-formalv-prim63_mathcomp" {= version}
+]
+
+build: [
+  [make "-C" "theories/check_range" "-j" "%{jobs}%"]
+]
+install: [
+  [make "-C" "theories/check_range" "install"]
+]
+
+url {
+  src: "https://gitlab.com/formalv/formalv/-/archive/1.3.0/formalv-1.3.0.tar.gz"
+  checksum: "sha256=a1045f3555371940e807046781e43702802560ef309c4be6cfe65088a8bf8347"
+}

released/packages/coq-formalv-prim63_mathcomp/coq-formalv-prim63_mathcomp.1.3.0/opam

@@ -0,0 +1,49 @@
+opam-version: "2.0"
+synopsis: "Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63" # One-line description
+description: """
+FV Prim63 to MathComp provides conversions from the Coq primitive integers
+Uint63 and Sint63 to the MathComp natural and integer numbers nat and int,
+and vice versa, as well as lemmas to rewrite between their respective
+operations.
+""" # Longer description, can span several lines
+
+homepage: "https://gitlab.com/formalv/formalv"
+dev-repo: "git+https://gitlab.com/formalv/formalv"
+bug-reports: "https://gitlab.com/formalv/formalv/-/issues"
+doc: "https://formalv.gitlab.io/formalv/coqdoc/toc.html"
+
+maintainer: "Mireia González Bedmar <[email protected]>"
+
+tags: [
+  "keyword:refinement"
+  "keyword:primitive integers"
+  "logpath:formalv.prim63_mathcomp"
+]
+
+authors: [
+  "Ana de Almeida Borges"
+  "Quim Casals Buñuel"
+  "Juan Conejero Rodriguez"
+  "Mireia González Bedmar"
+  "Eduardo Hermo Reyes"
+]
+
+license: "PolyForm Noncommercial License 1.0.0" # Make sure this is reflected by a LICENSE file in your sources
+
+depends: [
+  "coq" {>= "8.19" & < "8.20~"}
+  "coq-mathcomp-algebra" {>= "2.3" & < "2.4~" }
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4~" }
+]
+
+build: [
+  [make "-C" "theories/prim63_mathcomp" "-j" "%{jobs}%"]
+]
+install: [
+  [make "-C" "theories/prim63_mathcomp" "install"]
+]
+
+url {
+  src: "https://gitlab.com/formalv/formalv/-/archive/1.3.0/formalv-1.3.0.tar.gz"
+  checksum: "sha256=a1045f3555371940e807046781e43702802560ef309c4be6cfe65088a8bf8347"
+}

released/packages/coq-formalv-time/coq-formalv-time.1.3.0/opam

@@ -0,0 +1,53 @@
+opam-version: "2.0"
+synopsis: "A Coq library for time and date arithmetic according to the UTC standard with leap seconds" # One-line description
+description: """
+FV Time is a library for managing conversions between time formats (UTC and
+timestamps), as well as commonly used functions for time arithmetic. As a
+library for time conversions, its novelty is the implementation of leap
+seconds (which are part of the UTC standard but usually not implemented in
+commercial libraries).
+""" # Longer description, can span several lines
+
+homepage: "https://gitlab.com/formalv/formalv"
+dev-repo: "git+https://gitlab.com/formalv/formalv"
+bug-reports: "https://gitlab.com/formalv/formalv/-/issues"
+doc: "https://formalv.gitlab.io/formalv/coqdoc/toc.html"
+maintainer: "Mireia González Bedmar <[email protected]>"
+
+tags: [
+  "keyword:time"
+  "keyword:date"
+  "keyword:timestamp"
+  "logpath:formalv.time"
+]
+
+authors: [
+  "Ana de Almeida Borges"
+  "Quim Casals Buñuel"
+  "Juan Conejero Rodriguez"
+  "Mireia González Bedmar"
+  "Eduardo Hermo Reyes"
+]
+
+license: "PolyForm Noncommercial License 1.0.0" # Make sure this is reflected by a LICENSE file in your sources
+
+depends: [
+  "coq" {>= "8.19" & < "8.20~"}
+  "coq-mathcomp-algebra" {>= "2.3" & < "2.4~" }
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4~" }
+  "coq-formalv-prim63_mathcomp" {= version}
+  "coq-formalv-check_range" {= version}
+]
+
+build: [
+  [make "-C" "theories/time" "-j" "%{jobs}%"]
+]
+
+install: [
+  [make "-C" "theories/time" "install"]
+]
+
+url {
+  src: "https://gitlab.com/formalv/formalv/-/archive/1.3.0/formalv-1.3.0.tar.gz"
+  checksum: "sha256=a1045f3555371940e807046781e43702802560ef309c4be6cfe65088a8bf8347"
+}