Split into 3 opam packages

ArchSem/dune

@@ -7,7 +7,7 @@
    CandidateExecutions
    GenPromising
  )
- (theories SailStdpp ASCommon)
+ (theories stdpp Hammer RecordUpdate Equations Ltac2 SailStdpp ASCommon)
  (coqdoc_flags :standard --utf8
                --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp
                --external ../../Common/ASCommon.html ASCommon

ArchSemArm/dune

@@ -1,6 +1,6 @@
 (coq.theory
  (name ArchSemArm)
- (package coq-archsem)
+ (package coq-archsem-arm)
  (modules
    SailArmInstTypes
    ArmInst
@@ -13,7 +13,7 @@
    VMSA22Arm
    VMUMEquivThm
  )
- (theories ASCommon ArchSem)
+ (theories stdpp Hammer RecordUpdate Equations Ltac2 SailStdpp ASCommon ArchSem)
  (coqdoc_flags :standard --utf8
                --external https://plv.mpi-sws.org/coqdoc/stdpp stdpp
                --external ../../Common/ASCommon.html ASCommon

Common/dune

@@ -1,6 +1,6 @@
 (coq.theory
  (name ASCommon)
- (package coq-archsem)
+ (package coq-archsem-common)
  (modules
    Common
    CBase

Extraction/dune

@@ -16,5 +16,4 @@
 
 (library
   (name Archsem_ocaml) ; TODO might change
-  (public_name coq-archsem)
   (libraries zarith))

coq-archsem-arm.opam

@@ -0,0 +1,38 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis:
+  "Coq infrastructure to reason about hardware CPU architecture semantics, Arm instantiation"
+maintainer: ["Thibaut Pérami <[email protected]>"]
+authors: [
+  "Thibaut Pérami"
+  "Zonguyan Liu"
+  "Nils Lauermann"
+  "Jean Pichon-Pharabod"
+  "Brian Campbell"
+  "Alasdair Armstrong"
+  "Ben Simner"
+  "Peter Sewell"
+]
+license: "BSD-2-Clause"
+homepage: "https://github.com/rems-project/archsem"
+bug-reports: "https://github.com/rems-project/archsem/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "coq-archsem"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/rems-project/archsem.git"

coq-archsem-common.opam

@@ -0,0 +1,44 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis:
+  "Common infrastructure and definition for the ArchSem project, includes CDestruct and a free monad library"
+maintainer: ["Thibaut Pérami <[email protected]>"]
+authors: [
+  "Thibaut Pérami"
+  "Zonguyan Liu"
+  "Nils Lauermann"
+  "Jean Pichon-Pharabod"
+  "Brian Campbell"
+  "Alasdair Armstrong"
+  "Ben Simner"
+  "Peter Sewell"
+]
+license: "BSD-2-Clause"
+homepage: "https://github.com/rems-project/archsem"
+bug-reports: "https://github.com/rems-project/archsem/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "coq" {>= "8.19.2"}
+  "coq-stdlib"
+  "coq-equations" {>= "1.3"}
+  "coq-record-update" {>= "0.3.4"}
+  "coq-hammer-tactics" {>= "1.3.2"}
+  "coq-stdpp" {= "1.10.0"}
+  "coq-stdpp-bitvector" {= "1.10.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/rems-project/archsem.git"

coq-archsem.opam

@@ -1,7 +1,7 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis:
-  "Coq infrastructure to reason about hardware CPU architecture semantics"
+  "Coq infrastructure to reason about hardware CPU architecture semantics, architecture generic part"
 maintainer: ["Thibaut Pérami <[email protected]>"]
 authors: [
   "Thibaut Pérami"
@@ -18,13 +18,7 @@ homepage: "https://github.com/rems-project/archsem"
 bug-reports: "https://github.com/rems-project/archsem/issues"
 depends: [
   "dune" {>= "3.8"}
-  "coq" {>= "8.19.2"}
-  "coq-stdlib"
-  "coq-equations" {>= "1.3"}
-  "coq-record-update" {>= "0.3.4"}
-  "coq-hammer-tactics" {>= "1.3.2"}
-  "coq-stdpp" {= "1.10.0"}
-  "coq-stdpp-bitvector" {= "1.10.0"}
+  "coq-archsem-common"
   "coq-sail-stdpp" {dev}
   "odoc" {with-doc}
 ]

dune-project

@@ -17,8 +17,8 @@
 (maintainers "Thibaut Pérami <[email protected]>")
 
 (package
- (name coq-archsem)
- (synopsis "Coq infrastructure to reason about hardware CPU architecture semantics")
+ (name coq-archsem-common)
+ (synopsis "Common infrastructure and definition for the ArchSem project, includes CDestruct and a free monad library")
  (depends
   (coq (>= 8.19.2))
    coq-stdlib
@@ -27,8 +27,25 @@
   (coq-hammer-tactics (>= 1.3.2))
   (coq-stdpp (= 1.10.0))
   (coq-stdpp-bitvector (= 1.10.0))
+ )
+)
+
+(package
+ (name coq-archsem)
+ (synopsis "Coq infrastructure to reason about hardware CPU architecture semantics, architecture generic part")
+ (depends
+   coq-archsem-common ; need same commit
   (coq-sail-stdpp :dev) ; See INSTALL.md for the commit number
  )
 )
 
+(package
+ (name coq-archsem-arm)
+ (synopsis "Coq infrastructure to reason about hardware CPU architecture semantics, Arm instantiation")
+ (depends
+   coq-archsem
+ )
+)
+
+
 (generate_opam_files)