chore: generate opam files from dune-package

dune-project

@@ -1,3 +1,82 @@
 (lang dune 2.0)
 
+(generate_opam_files true)
+
+(license Apache)
+
+(authors "Simon Cruanes" "Guillaume Bury")
+
+(maintainers "simon.cruanes.2007@m4x.org")
+
+(version dev)
+
+(homepage "https://github.com/c-cube/sidekick")
+
+(source
+ (github c-cube/sidekick))
+
+(bug_reports "https://github.com/c-cube/sidekick/issues/")
+
 (using menhir 1.0)
+
+(package
+ (name sidekick)
+ (synopsis "SMT solver based on msat and CDCL(T) (core library)")
+ (depends
+  (containers
+   (and
+    (>= 3.6)
+    (< 4.0)))
+  (iter
+   (>= 1.0))
+  (zarith :with-test)
+  (alcotest :with-test)
+  (odoc :with-doc))
+ (depopts
+  mtime ; for profiling stuff
+  memtrace ; memory profiling
+  zarith ; for arith
+  )
+ (tags
+  ("sat" "smt"))
+ (conflicts
+  (zarith
+   (< 1.8))
+  ; need infix ops
+  ))
+
+(package
+ (name sidekick-base)
+ (synopsis "Concrete terms and theories for sidekick")
+ (depends
+  zarith
+  (smtlib-utils
+   (and
+    (>= "0.1")
+    (< "0.4")))
+  (sidekick
+   (= :version))
+  (sidekick-base
+   (= :version))
+  (qcheck
+   (and
+    :with-test
+    (>= 0.16)))
+  (mdx :with-test)
+  (odoc :with-doc)
+  menhir))
+
+(package
+ (name sidekick-bin)
+ (synopsis "SMT solver based on msat and CDCL(T) (standalone binary)")
+ (depends
+  zarith
+  (smtlib-utils
+   (and
+    (>= "0.1")
+    (< "0.4")))
+  (sidekick
+   (= :version))
+  (sidekick-base
+   (= :version))
+  menhir))

sidekick-base.opam

@@ -1,30 +1,35 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "sidekick-base"
-license: "Apache"
-synopsis: "Standalone term definition for the SMT solver library sidekick"
 version: "dev"
-author: ["Simon Cruanes"]
+synopsis: "Concrete terms and theories for sidekick"
 maintainer: ["simon.cruanes.2007@m4x.org"]
-build: [
+authors: ["Simon Cruanes" "Guillaume Bury"]
-  ["dune" "build" "@install" "-p" name "-j" jobs]
+license: "Apache"
-  ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
-  ["dune" "runtest" "-p" name "-j" jobs] {with-test}
-]
-depends: [
-  "dune" { >= "1.1" }
-  "containers" { >= "3.0" & < "4.0" }
-  "iter" { >= "1.0" & < "2.0" }
-  "ocaml" { >= "4.08" } # for BARE, which uses Bytes functions
-  "sidekick" { = version }
-  "zarith" { >= "1.8" } # constraint for infix ops
-  "alcotest" {with-test}
-  "qcheck" {with-test & >= "0.16" }
-  "odoc" {with-doc}
-  "mdx" {with-test}
-  # "bare_encoding" {with-doc}
-]
-tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
-dev-repo: "git+https://github.com/c-cube/sidekick.git"
 bug-reports: "https://github.com/c-cube/sidekick/issues/"
-
+depends: [
+  "dune" {>= "2.0"}
+  "zarith"
+  "smtlib-utils" {>= "0.1" & < "0.4"}
+  "sidekick" {= version}
+  "sidekick-base" {= version}
+  "qcheck" {with-test & >= "0.16"}
+  "mdx" {with-test}
+  "odoc" {with-doc}
+  "menhir"
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/c-cube/sidekick.git"

sidekick-bin.opam

@@ -1,33 +1,32 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "sidekick-bin"
-license: "Apache"
-synopsis: "SMT solver based on msat and CDCL(T) (standalone binary)"
 version: "dev"
-author: ["Simon Cruanes" "Guillaume Bury"]
+synopsis: "SMT solver based on msat and CDCL(T) (standalone binary)"
 maintainer: ["simon.cruanes.2007@m4x.org"]
-build: [
+authors: ["Simon Cruanes" "Guillaume Bury"]
-  ["dune" "build" "@install" "-p" name "-j" jobs]
+license: "Apache"
-  ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
-  # ["dune" "runtest" "-p" name] {with-test}
-]
-depends: [
-  "dune" { >= "1.1" }
-  "containers" { >= "3.0" & < "4.0" }
-  "iter" { >= "1.0" & < "2.0" }
-  "zarith"
-  "smtlib-utils" { >= "0.1" & < "0.4" }
-  "sidekick" { = version }
-  "sidekick-base" { = version }
-  "menhir"
-  "ocaml" { >= "4.08" }
-  "odoc" {with-doc}
-]
-depopts: [
-  "memtrace"
-  "mtime"
-]
-tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
-dev-repo: "git+https://github.com/c-cube/sidekick.git"
 bug-reports: "https://github.com/c-cube/sidekick/issues/"
-
+depends: [
+  "dune" {>= "2.0"}
+  "zarith"
+  "smtlib-utils" {>= "0.1" & < "0.4"}
+  "sidekick" {= version}
+  "sidekick-base" {= version}
+  "menhir"
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/c-cube/sidekick.git"

sidekick.opam

@@ -1,35 +1,37 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "sidekick"
-license: "Apache"
-synopsis: "SMT solver based on msat and CDCL(T) (functor library)"
 version: "dev"
-author: ["Simon Cruanes" "Guillaume Bury"]
+synopsis: "SMT solver based on msat and CDCL(T) (core library)"
 maintainer: ["simon.cruanes.2007@m4x.org"]
-build: [
+authors: ["Simon Cruanes" "Guillaume Bury"]
-  ["dune" "subst"] {dev}
+license: "Apache"
-  ["dune" "build" "@install" "-p" name "-j" jobs]
+tags: ["sat" "smt"]
-  ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
+homepage: "https://github.com/c-cube/sidekick"
-  ["dune" "runtest" "-p" name "-j" jobs] {with-test}
+bug-reports: "https://github.com/c-cube/sidekick/issues/"
-]
 depends: [
-  "dune" { >= "2.0" }
+  "dune" {>= "2.0"}
-  "containers" { >= "3.6" & < "4.0" }
+  "containers" {>= "3.6" & < "4.0"}
-  "iter" { >= "1.0" & < "2.0" }
+  "iter" {>= "1.0"}
-  "ocaml" { >= "4.08" }
+  "zarith" {with-test}
-  "zarith" { with-test }
   "alcotest" {with-test}
   "odoc" {with-doc}
 ]
-depopts: [
+depopts: ["mtime" "memtrace" "zarith"]
-  "mtime"   # for profiling stuff
-  "memtrace" # memory profiling
-  "zarith" # for arithmetic
-]
 conflicts: [
-  "zarith" { < "1.8" } # for infix ops
+  "zarith" {< "1.8"}
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
-tags: [ "sat" "smt" ]
-homepage: "https://github.com/c-cube/sidekick"
 dev-repo: "git+https://github.com/c-cube/sidekick.git"
-bug-reports: "https://github.com/c-cube/sidekick/issues/"
-