Merge pull request #3358 from Lysxia/master

Release coq-simple-io.1.11.0, coq-itree.5.2.1, coq-quickchick.2.1.0

Author: palmskog

released/packages/coq-itree/coq-itree.5.2.1/opam

@@ -0,0 +1,35 @@
+opam-version: "2.0"
+synopsis: "Library for representing recursive and impure programs with equational reasoning"
+maintainer: ["Li-yao Xia <[email protected]>"]
+authors: [
+  "Li-yao Xia"
+  "Yannick Zakowski"
+  "Paul He"
+  "Chung-Kil Hur"
+  "Gregory Malecha"
+  "Steve Zdancewic"
+  "Benjamin Pierce"
+]
+license: "MIT"
+homepage: "https://github.com/DeepSpec/InteractionTrees"
+bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
+dev-repo: "git+https://github.com/DeepSpec/InteractionTrees.git"
+build: [
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test}]
+]
+depends: [
+  "dune" {>= "3.14"}
+  "coq" {>= "8.14"}
+  "coq-ext-lib" {>= "0.11.1"}
+  "coq-paco" {>= "4.2.1"}
+]
+tags: [
+  "org:deepspec"
+  "logpath:ITree"
+  "date:2025-02-28"
+]
+url {
+  http: "https://github.com/DeepSpec/InteractionTrees/archive/5.2.1.tar.gz"
+  checksum: "sha512=8027de84ad96c89887051e2df4d8e68cac87389d353936a5f56f4910277d2e78fdd3447d8ce6b0704ecda8880692392cf9331f529de516d0e7ee6918aea3f8a5"
+}

released/packages/coq-quickchick/coq-quickchick.2.1.0/opam

@@ -0,0 +1,64 @@
+opam-version: "2.0"
+synopsis: "Randomized Property-Based Testing for Coq"
+description: """\
+A library for property-based testing in Coq.
+
+  - Combinators for testable properties and random generators.
+  - QuickChick plugin for running tests in a Coq session.
+  - Includes a mutation testing tool."""
+maintainer: "[email protected]"
+authors: [
+  "Leonidas Lampropoulos"
+  "Zoe Paraskevopoulou"
+  "Maxime Denes"
+  "Catalin Hritcu"
+  "Benjamin Pierce"
+  "Li-yao Xia"
+  "Arthur Azevedo de Amorim"
+  "Yishuai Li"
+  "Antal Spector-Zabusky"
+]
+license: "MIT"
+homepage: "https://github.com/QuickChick/QuickChick"
+bug-reports: "https://github.com/QuickChick/QuickChick/issues"
+depends: [
+  "dune" {>= "3.12"}
+  "ocaml" {>= "4.07"}
+  "menhir" {build}
+  "cppo" {build & >= "1.6.8"}
+  "coq" {>= "8.15~"}
+  "coq-ext-lib"
+  "coq-mathcomp-ssreflect"
+  "coq-simple-io" {>= "1.6.0"}
+  "ocamlfind"
+  "ocamlbuild"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+    "--stop-on-first-error"
+  ]
+]
+dev-repo: "git+https://github.com/QuickChick/QuickChick.git"
+tags: [
+  "keyword:testing"
+  "logpath:QuickChick"
+  "date:2025-02-28"
+]
+url {
+  src:
+    "https://github.com/QuickChick/QuickChick/archive/v2.1.0.tar.gz"
+  checksum: [
+    "sha512=d8077402192b95e9595f523e6dc499179062bc9a12718843dfef57ff6bdfe559f7d2276c2e0a33567fea2e10252f766851ae7f3bece33122920af2fc52510e76"
+  ]
+}

released/packages/coq-simple-io/coq-simple-io.1.11.0/opam

@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "Li-yao Xia <[email protected]>"
+authors: [ "Li-yao Xia" "Yishuai Li" ]
+homepage: "https://github.com/Lysxia/coq-simple-io"
+bug-reports: "https://github.com/Lysxia/coq-simple-io/issues"
+license: "MIT"
+dev-repo: "git+https://github.com/Lysxia/coq-simple-io.git"
+build: [
+  ["dune" "subst"] {dev}
+  [ "dune" "build" "-p" name "-j" jobs "@install" ]
+]
+depends: [
+  "dune" {>= "3.7"}
+  "ocaml" {>= "4.08.0"}
+  "ocamlfind"
+  "coq" {>= "8.12~" & < "9.1~"}
+  "coq-ext-lib" {>= "0.10.0"}
+  "ocamlbuild" {with-test & >= "0.9.0"}
+  "cppo" {build & >= "1.6.8"}
+]
+tags: [
+  "date:2025-02-28"
+  "logpath:SimpleIO"
+  "keyword:extraction"
+  "keyword:effects"
+]
+synopsis: "IO monad for Coq"
+description: """
+This library provides tools to implement IO programs directly in Coq, in a
+similar style to Haskell. Facilities for formal verification are not included.
+
+IO is defined as a parameter with a purely functional interface in Coq,
+to be extracted to OCaml. Some wrappers for the basic types and functions in
+the OCaml Stdlib module are provided. Users are free to define their own
+APIs on top of this IO type."""
+url {
+  src: "https://github.com/Lysxia/coq-simple-io/archive/1.11.0.tar.gz"
+  checksum: "sha512=814fb420609d081db03be7b8965f6d272e1bb41d8c7ec7d509dde34b6a994e8bc62d08b1d799746ecf121f557613bc5948eed2fd5d46b562b5873262b030728c"
+}