From da4dd1e2078f8838fff8c1aa66163650d6ccf51e Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Thu, 16 Jan 2025 13:57:19 +0100 Subject: [PATCH 1/9] releasing fcsl-pcm v2.1.0 --- .../coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam new file mode 100644 index 000000000..b51fbad7f --- /dev/null +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -0,0 +1,45 @@ +opam-version: "2.0" +maintainer: "fcsl@software.imdea.org" + +homepage: "https://github.com/imdea-software/fcsl-pcm" +dev-repo: "git+https://github.com/imdea-software/fcsl-pcm.git" +bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues" +license: "Apache-2.0" + +synopsis: "Coq library of Partial Commutative Monoids" +description: """ +The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), +a common algebraic structure used in separation logic for verification of +pointer-manipulating sequential and concurrent programs. + +The library provides lemmas for mechanised and automated reasoning about PCMs +in the abstract, but also supports concrete common PCM instances, such as heaps, +histories, and mutexes. + +This library relies on propositional and functional extentionality axioms.""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") } + "coq-mathcomp-algebra" +] + +tags: [ + "category:Computer Science/Data Types and Data Structures" + "keyword:partial commutative monoids" + "keyword:separation logic" + "keyword:concurrency" + "logpath:pcm" +] +authors: [ + "Aleksandar Nanevski" + "Anton Trunov" + "Alexander Gryzlov" +] +url { + src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" + checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" +} \ No newline at end of file From 1c1e3b98c0edfbb17369bc11bb8b5e7c78babbb9 Mon Sep 17 00:00:00 2001 From: Alekandar Nanevski Date: Thu, 16 Jan 2025 18:18:47 +0100 Subject: [PATCH 2/9] fixing ci issues --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index b51fbad7f..160b22706 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -40,6 +40,6 @@ authors: [ "Alexander Gryzlov" ] url { - src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" + src: "https://github.com/imdea-software/fcsl-pcm/archive/refs/tags/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" } \ No newline at end of file From 6465db6813f2ee980d9cb242c9392e424279907b Mon Sep 17 00:00:00 2001 From: Alekandar Nanevski Date: Thu, 16 Jan 2025 18:21:35 +0100 Subject: [PATCH 3/9] fixing ci --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index 160b22706..b51fbad7f 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -40,6 +40,6 @@ authors: [ "Alexander Gryzlov" ] url { - src: "https://github.com/imdea-software/fcsl-pcm/archive/refs/tags/v2.1.0.tar.gz" + src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" } \ No newline at end of file From 5eee45f7fbb11d5edc02dfe97cf102dccc21dfe0 Mon Sep 17 00:00:00 2001 From: Alekandar Nanevski Date: Thu, 16 Jan 2025 18:26:41 +0100 Subject: [PATCH 4/9] fixing --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index b51fbad7f..542a9a6fe 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -42,4 +42,4 @@ authors: [ url { src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" -} \ No newline at end of file +} From c759640ed544fe9ed61d478dcc122be645f2f44f Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Thu, 16 Jan 2025 18:31:22 +0100 Subject: [PATCH 5/9] try to fix CI artifact issues --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d7c24030b..e7e61eb92 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -40,7 +40,7 @@ jobs: cp coq-packages.json dest - name: Upload Pages artifact - uses: actions/upload-pages-artifact@v2 + uses: actions/upload-pages-artifact@v3 with: path: dest From 328b6c3af94f57dd5f7479c0dab7a4f1ec554fea Mon Sep 17 00:00:00 2001 From: Alekandar Nanevski Date: Thu, 16 Jan 2025 18:37:36 +0100 Subject: [PATCH 6/9] releasing fcsl-pcm v2.1.0 --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 1 + 1 file changed, 1 insertion(+) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index 542a9a6fe..d46a6a120 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -43,3 +43,4 @@ url { src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" } + From 455a6f46d138d1e130ae8e131b770b912523f41b Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Thu, 16 Jan 2025 20:13:19 +0100 Subject: [PATCH 7/9] Update released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index d46a6a120..3931b38c7 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -40,7 +40,7 @@ authors: [ "Alexander Gryzlov" ] url { - src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" + src: "https://github.com/imdea-software/fcsl-pcm/archive/refs/tags/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" } From 2f3de27662171dc9f1a4141877b5bfaf57622de1 Mon Sep 17 00:00:00 2001 From: Alekandar Nanevski Date: Thu, 16 Jan 2025 20:14:16 +0100 Subject: [PATCH 8/9] fixing sha --- released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam index d46a6a120..3931b38c7 100644 --- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam +++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam @@ -40,7 +40,7 @@ authors: [ "Alexander Gryzlov" ] url { - src: "https://github.com/imdea-software/fcsl-pcm/archive/v2.1.0.tar.gz" + src: "https://github.com/imdea-software/fcsl-pcm/archive/refs/tags/v2.1.0.tar.gz" checksum: "sha256=019ef65ce51b12c623d5c6cc8f98f3499cf3bc5bd273c67097c6106ad082780b" } From 8efaa4602111ac8885a5150b6c7c511336da71f7 Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Fri, 17 Jan 2025 15:44:19 +0100 Subject: [PATCH 9/9] releacing coq-htt-core and coq-htt v2.1.0 --- .../coq-htt-core/coq-htt-core.2.1.0/opam | 59 ++++++++++++++++++ released/packages/coq-htt/coq-htt.2.1.0/opam | 60 +++++++++++++++++++ 2 files changed, 119 insertions(+) create mode 100644 released/packages/coq-htt-core/coq-htt-core.2.1.0/opam create mode 100644 released/packages/coq-htt/coq-htt.2.1.0/opam diff --git a/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam b/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam new file mode 100644 index 000000000..7c5d18b17 --- /dev/null +++ b/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam @@ -0,0 +1,59 @@ +opam-version: "2.0" +maintainer: "fcsl@software.imdea.org" + +homepage: "https://github.com/imdea-software/htt" +dev-repo: "git+https://github.com/imdea-software/htt.git" +bug-reports: "https://github.com/imdea-software/htt/issues" +license: "Apache-2.0" + +synopsis: "Hoare Type Theory" +description: """ +Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating +programs based on Separation logic. + +HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A +Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition +`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads, +as used in the programming language Haskell. Monads hygienically combine the language features +for pure functional programming, with those for imperative programming, such as state or +exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard +isomorphism between monads and (functional programming variant of) Separation logic. Every +effectful command in HTT has a type that corresponds to the appropriate non-structural inference +rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a +command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for +sequential composition, and the type for monadic unit combines the Hoare rules for the idle +program (in a small-footprint variant) and for variable assignment (adapted for functional +variables). The connection reconciles dependent types with effects of state and exceptions and +establishes Separation logic as a type theory for such effects. In implementation terms, it means +that HTT implements Separation logic as a shallow embedding in Coq.""" + +build: [make "-C" "htt" "-j%{jobs}%"] +install: [make "-C" "htt" "install"] +depends: [ + "dune" {>= "3.6"} + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq-mathcomp-algebra" + "coq-mathcomp-fingroup" + "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } +] + +tags: [ + "category:Computer Science/Data Types and Data Structures" + "keyword:partial commutative monoids" + "keyword:separation logic" + "logpath:htt" +] + +authors: [ + "Aleksandar Nanevski" + "Germán Andrés Delbianco" + "Alexander Gryzlov" + "Marcos Grandury" +] + +url { + src: "https://github.com/imdea-software/htt/archive/refs/tags/v2.1.0.tar.gz" + checksum: "sha256=e2819211c05a011f8101d006865c642a513c3e581810f590d8d8d7a651046b05" +} + diff --git a/released/packages/coq-htt/coq-htt.2.1.0/opam b/released/packages/coq-htt/coq-htt.2.1.0/opam new file mode 100644 index 000000000..64a2616b4 --- /dev/null +++ b/released/packages/coq-htt/coq-htt.2.1.0/opam @@ -0,0 +1,60 @@ +opam-version: "2.0" +maintainer: "fcsl@software.imdea.org" + +homepage: "https://github.com/imdea-software/htt" +dev-repo: "git+https://github.com/imdea-software/htt.git" +bug-reports: "https://github.com/imdea-software/htt/issues" +license: "Apache-2.0" + +synopsis: "Hoare Type Theory" +description: """ +Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating +programs based on Separation logic. + +HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A +Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition +`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads, +as used in the programming language Haskell. Monads hygienically combine the language features +for pure functional programming, with those for imperative programming, such as state or +exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard +isomorphism between monads and (functional programming variant of) Separation logic. Every +effectful command in HTT has a type that corresponds to the appropriate non-structural inference +rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a +command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for +sequential composition, and the type for monadic unit combines the Hoare rules for the idle +program (in a small-footprint variant) and for variable assignment (adapted for functional +variables). The connection reconciles dependent types with effects of state and exceptions and +establishes Separation logic as a type theory for such effects. In implementation terms, it means +that HTT implements Separation logic as a shallow embedding in Coq.""" + +build: [make "-C" "examples" "-j%{jobs}%"] +install: [make "-C" "examples" "install"] +depends: [ + "dune" {>= "3.6"} + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq-mathcomp-algebra" + "coq-mathcomp-fingroup" + "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } + "coq-htt-core" {= version} +] + +tags: [ + "category:Computer Science/Data Types and Data Structures" + "keyword:partial commutative monoids" + "keyword:separation logic" + "logpath:htt" +] + +authors: [ + "Aleksandar Nanevski" + "Germán Andrés Delbianco" + "Alexander Gryzlov" + "Marcos Grandury" +] + +url { + src: "https://github.com/imdea-software/htt/archive/refs/tags/v2.1.0.tar.gz" + checksum: "sha256=e2819211c05a011f8101d006865c642a513c3e581810f590d8d8d7a651046b05" +} +