make coq-htt package depend on coq-htt-core

.github/workflows/docker-action.yml

@@ -1,5 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-
 name: Docker CI
 
 on:
@@ -22,12 +20,34 @@ jobs:
           - 'mathcomp/mathcomp:latest-coq-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-htt.opam'
           custom_image: ${{ matrix.image }}
-
+          custom_script: |
+            {{before_install}}
+            startGroup "Build htt-core dependencies"
+              opam pin add -n -y -k path coq-htt-core .
+              opam update -y
+              opam install -y -j $(nproc) coq-htt-core --deps-only
+            endGroup
+            startGroup "Build htt-core"
+              opam install -y -v -j $(nproc) coq-htt-core
+              opam list
+            endGroup
+            startGroup "Build htt dependencies"
+              opam pin add -n -y -k path coq-htt .
+              opam update -y
+              opam install -y -j $(nproc) coq-htt --deps-only
+            endGroup
+            startGroup "Build coq-htt"
+              opam install -y -v -j $(nproc) coq-htt
+              opam list
+            endGroup
+            startGroup "Uninstallation test"
+              opam remove -y coq-htt
+              opam remove -y coq-htt-core
+            endGroup
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

coq-htt.opam

@@ -1,5 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -30,14 +28,15 @@ 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: [make "-j%{jobs}%"]
-install: [make "install"]
+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-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
+  "coq-htt-core" {= version}
 ]
 
 tags: [

examples/dune

@@ -0,0 +1,9 @@
+(coq.theory
+ (name htt)
+ (package coq-htt)
+ (synopsis "Hoare Type Theory with examples")
+ (flags :standard
+   -w -notation-overridden
+   -w -local-declaration
+   -w -redundant-canonical-projection
+   -w -projection-no-head-constant))