From be23bc6a40cbcce8b42d991033985723d584c472 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Oct 2021 11:23:12 -0400
Subject: [PATCH] update package descriptions
---
coq-iris-heap-lang.opam | 6 +++++-
coq-iris.opam | 17 +++++++++++++++--
2 files changed, 20 insertions(+), 3 deletions(-)
diff --git a/coq-iris-heap-lang.opam b/coq-iris-heap-lang.opam
index 7a6809ef3..7d671368c 100644
--- a/coq-iris-heap-lang.opam
+++ b/coq-iris-heap-lang.opam
@@ -9,8 +9,12 @@ version: "dev"
synopsis: "The canonical example language for Iris"
description: """
-This package provides the iris.heap_lang Coq module.
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
"""
+tags: [
+ "logpath:iris.heap_lang"
+]
depends: [
"coq-iris" {= version}
diff --git a/coq-iris.opam b/coq-iris.opam
index f098ca7f4..125b0e844 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -9,9 +9,22 @@ version: "dev"
synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
description: """
-This package provides the following Coq modules:
-iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
"""
+tags: [
+ "logpath:iris.prelude"
+ "logpath:iris.algebra"
+ "logpath:iris.si_logic"
+ "logpath:iris.bi"
+ "logpath:iris.proofmode"
+ "logpath:iris.base_logic"
+ "logpath:iris.program_logic"
+]
depends: [
"coq" { (>= "8.12" & < "8.15~") | (= "dev") }
--
GitLab