Skip to content

Commit

Permalink
playing with dune
Browse files Browse the repository at this point in the history
  • Loading branch information
aleksnanevski committed Sep 27, 2024
1 parent 03220f8 commit be7aaa8
Show file tree
Hide file tree
Showing 7 changed files with 6 additions and 110 deletions.
53 changes: 0 additions & 53 deletions coq-htt-examples.opam

This file was deleted.

5 changes: 2 additions & 3 deletions coq-htt.opam
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
# 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]"
Expand Down Expand Up @@ -31,9 +30,9 @@ variables). The connection reconciles dependent types with effects of state 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]
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"dune" {>= "3.6"}
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
"coq-mathcomp-algebra"
Expand Down
2 changes: 1 addition & 1 deletion htt/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

(coq.theory
(name htt)
(package coq-htt)
(package coq-htt-core)
(synopsis "Hoare Type Theory")
(flags :standard
-w -notation-overridden
Expand Down
2 changes: 1 addition & 1 deletion meta.yml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
fullname: Hoare Type Theory
shortname: htt
organization: imdea-software
opam_name: coq-htt
opam_name: coq-htt-core
community: false
action: true
dune: true
Expand Down
2 changes: 1 addition & 1 deletion regenerate.sh
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#!/usr/bin/env bash

TMP=$(mktemp -d); git clone https://github.com/coq-community/templates.git $TMP
$TMP/generate.sh README.md coq-htt.opam dune-project
$TMP/generate.sh README.md coq-htt-core.opam dune-project

echo "Proceeding with customized generation..."

Expand Down
50 changes: 0 additions & 50 deletions templates-extra/coq-htt-examples.opam.mustache

This file was deleted.

2 changes: 1 addition & 1 deletion templates-extra/dune.mustache
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@
-w -notation-overridden
-w -local-declaration
-w -redundant-canonical-projection
-w -projection-no-head-constant))
-w -projection-no-head-constant))

0 comments on commit be7aaa8

Please sign in to comment.