From 7057d6df09c785c217e6f2abde65f2358522cbca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Feb 2026 19:21:44 -0800 Subject: [PATCH 1/2] Add opam files for all SF volumes Co-Authored-By: Claude Opus 4.6 --- coq-sf-lf.opam | 36 ++++++++++++++++++++++++++++++++++++ coq-sf-plf.opam | 36 ++++++++++++++++++++++++++++++++++++ coq-sf-qc.opam | 36 ++++++++++++++++++++++++++++++++++++ coq-sf-slf.opam | 36 ++++++++++++++++++++++++++++++++++++ coq-sf-vc.opam | 36 ++++++++++++++++++++++++++++++++++++ coq-sf-vfa.opam | 36 ++++++++++++++++++++++++++++++++++++ 6 files changed, 216 insertions(+) create mode 100644 coq-sf-lf.opam create mode 100644 coq-sf-plf.opam create mode 100644 coq-sf-qc.opam create mode 100644 coq-sf-slf.opam create mode 100644 coq-sf-vc.opam create mode 100644 coq-sf-vfa.opam diff --git a/coq-sf-lf.opam b/coq-sf-lf.opam new file mode 100644 index 000000000..671d6460c --- /dev/null +++ b/coq-sf-lf.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "lf-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "lf-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "Logical Foundations (Volume 1 of Software Foundations)" +description: + "Logical Foundations is the entry-point to the series, covering functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz" +} diff --git a/coq-sf-plf.opam b/coq-sf-plf.opam new file mode 100644 index 000000000..0e961ad0a --- /dev/null +++ b/coq-sf-plf.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "plf-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "plf-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "Programming Language Foundations (Volume 2 of Software Foundations)" +description: + "Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz" +} diff --git a/coq-sf-qc.opam b/coq-sf-qc.opam new file mode 100644 index 000000000..5f69032a7 --- /dev/null +++ b/coq-sf-qc.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "qc-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "qc-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "QuickChick: Property-Based Testing in Coq (Volume 4 of Software Foundations)" +description: + "QuickChick introduces tools for combining randomized property-based testing with formal specification and proof in Coq." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/qc-current/qc.tgz" +} diff --git a/coq-sf-slf.opam b/coq-sf-slf.opam new file mode 100644 index 000000000..9762a280a --- /dev/null +++ b/coq-sf-slf.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "slf-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "slf-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "Separation Logic Foundations (Volume 6 of Software Foundations)" +description: + "Separation Logic Foundations is an in-depth introduction to separation logic, a practical approach to modular verification of imperative programs." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/slf-current/slf.tgz" +} diff --git a/coq-sf-vc.opam b/coq-sf-vc.opam new file mode 100644 index 000000000..55d3ee9c4 --- /dev/null +++ b/coq-sf-vc.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "vc-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "vc-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "Verifiable C (Volume 5 of Software Foundations)" +description: + "Verifiable C is an extended hands-on tutorial on specifying and verifying real-world C programs using the Princeton Verified Software Toolchain." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/vc-current/vc.tgz" +} diff --git a/coq-sf-vfa.opam b/coq-sf-vfa.opam new file mode 100644 index 000000000..76a45daa1 --- /dev/null +++ b/coq-sf-vfa.opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +homepage: "https://softwarefoundations.cis.upenn.edu/" +doc: "https://softwarefoundations.cis.upenn.edu/" +authors: [ + "Benjamin C. Pierce" + "Arthur Azevedo de Amorim" + "Chris Casinghino" + "Marco Gaboardi" + "Michael Greenberg" + "Cătălin Hriţcu" + "Vilhelm Sjöberg" + "Andrew Tolmach" + "Brent Yorgey" +] +license: "like MIT" + +build: [ + [make "-C" "vfa-current" "-j%{jobs}%"] +] + +install: [ + [make "-C" "vfa-current" "install"] +] + +bug-reports: "?" +depends: [ + "ocaml" + "coq" +] +synopsis: + "Verified Functional Algorithms (Volume 3 of Software Foundations)" +description: + "Verified Functional Algorithms demonstrates how fundamental data structures can be formally specified and mechanically verified." +url { + src: "https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz" +} From e72562e16872bc91d5f4f96584cf4ad127287b21 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Feb 2026 20:32:35 -0800 Subject: [PATCH 2/2] Add external dependencies to qc and vc opam files Co-Authored-By: Claude Opus 4.6 --- coq-sf-qc.opam | 1 + coq-sf-vc.opam | 1 + 2 files changed, 2 insertions(+) diff --git a/coq-sf-qc.opam b/coq-sf-qc.opam index 5f69032a7..31ebbf488 100644 --- a/coq-sf-qc.opam +++ b/coq-sf-qc.opam @@ -26,6 +26,7 @@ bug-reports: "?" depends: [ "ocaml" "coq" + "coq-quickchick" ] synopsis: "QuickChick: Property-Based Testing in Coq (Volume 4 of Software Foundations)" diff --git a/coq-sf-vc.opam b/coq-sf-vc.opam index 55d3ee9c4..af35d35ce 100644 --- a/coq-sf-vc.opam +++ b/coq-sf-vc.opam @@ -26,6 +26,7 @@ bug-reports: "?" depends: [ "ocaml" "coq" + "coq-vst" ] synopsis: "Verifiable C (Volume 5 of Software Foundations)"