From 2f96f36e7597f1779379d9e26d75f200de364213 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 6 Oct 2022 19:51:43 -0400 Subject: [PATCH] chore: generate opam files from dune-package --- dune-project | 79 ++++++++++++++++++++++++++++++++++++++++++++++ sidekick-base.opam | 55 +++++++++++++++++--------------- sidekick-bin.opam | 55 ++++++++++++++++---------------- sidekick.opam | 52 +++++++++++++++--------------- 4 files changed, 163 insertions(+), 78 deletions(-) diff --git a/dune-project b/dune-project index 68167760..4ec7b415 100644 --- a/dune-project +++ b/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)) diff --git a/sidekick-base.opam b/sidekick-base.opam index 2db7f48d..49d78b74 100644 --- a/sidekick-base.opam +++ b/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: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - ["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" ] +authors: ["Simon Cruanes" "Guillaume Bury"] +license: "Apache" 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" diff --git a/sidekick-bin.opam b/sidekick-bin.opam index 10a1bc57..81b78cca 100644 --- a/sidekick-bin.opam +++ b/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: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - ["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" ] +authors: ["Simon Cruanes" "Guillaume Bury"] +license: "Apache" 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" diff --git a/sidekick.opam b/sidekick.opam index 7f263dca..c82c4a08 100644 --- a/sidekick.opam +++ b/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: [ - ["dune" "subst"] {dev} - ["dune" "build" "@install" "-p" name "-j" jobs] - ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc} - ["dune" "runtest" "-p" name "-j" jobs] {with-test} -] +authors: ["Simon Cruanes" "Guillaume Bury"] +license: "Apache" +tags: ["sat" "smt"] +homepage: "https://github.com/c-cube/sidekick" +bug-reports: "https://github.com/c-cube/sidekick/issues/" depends: [ - "dune" { >= "2.0" } - "containers" { >= "3.6" & < "4.0" } - "iter" { >= "1.0" & < "2.0" } - "ocaml" { >= "4.08" } - "zarith" { with-test } + "dune" {>= "2.0"} + "containers" {>= "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 arithmetic -] +depopts: ["mtime" "memtrace" "zarith"] 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/" -