forgot some files

coq-htt-core.opam

@@ -0,0 +1,54 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+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: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+ "dune" {>= "3.6"}
+ "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+ "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+ "coq-mathcomp-algebra" 
+ "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "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"
+]

templates-extra/coq-htt.opam.mustache

@@ -0,0 +1,50 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+
+opam-version: "2.0"
+maintainer: "{{& opam-file-maintainer }}{{^ opam-file-maintainer }}[email protected]{{/ opam-file-maintainer }}"
+version: "{{ opam-file-version }}{{^ opam-file-version }}dev{{/ opam-file-version }}"
+
+homepage: "https://github.com/{{ organization }}/{{ shortname }}"
+dev-repo: "git+https://github.com/{{ organization }}/{{ shortname }}.git"
+bug-reports: "https://github.com/{{ organization }}/{{ shortname }}/issues"{{# coqdoc }}
+doc: "https://{{ organization }}.github.io/{{ shortname }}/"{{/ coqdoc }}
+{{# license }}license: "{{ identifier }}"{{/ license }}
+
+synopsis: "{{& synopsis }}"
+description: """
+{{& description }}"""
+
+build: [make "-j%{jobs}%"{{# make_target }} "{{ make_target }}"{{/ make_target }}]
+{{# test_target }}
+run-test: [make "-j%{jobs}%" "{{ test_target }}"]
+{{/ test_target }}
+install: [make "install"{{# install_flag }} "{{ install_flag }}"{{/ install_flag }}]
+depends: [
+{{# supported_ocaml_versions }}
+ "ocaml" {{& opam }}
+{{/ supported_ocaml_versions }}
+ "coq" {{& supported_coq_versions.opam }}
+{{# dependencies }}
+{{# opam }}
+ "{{ name }}" {{& version }}
+{{/ opam }}
+{{/ dependencies }}
+]
+
+tags: [
+{{# categories }}
+ "category:{{ name }}"
+{{/ categories }}
+{{# keywords }}
+ "keyword:{{& name }}"
+{{/ keywords }}
+{{# date }}
+ "date:{{ date }}"
+{{/ date }}
+ "logpath:{{ namespace }}"
+]
+authors: [
+{{# authors }}
+ "{{& name }}{{# email }} <{{& email }}>{{/ email }}"
+{{/ authors }}
+]