smtml/dune-project at main · formalsec/smtml · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(lang dune 3.20)

(using menhir 2.1)

(using mdx 0.2)

(using dune_site 0.1)

(name smtml)

(version 0.26.0)

(generate_opam_files true)

(implicit_transitive_deps false-if-hidden-includes-supported)

(source (github formalsec/smtml))

(license "MIT")

(authors
 "João Pereira <joaomhmpereira@tecnico.ulisboa.pt>"
 "Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>"
 "Hichem Rami Ait El Hara <hra@ocamlpro.com>"
 "redianthus <redopam@pm.me>"
 "Arthur Carcano <arthur.carcano@ocamlpro.com>"
 "Pierre Chambart <pierre.chambart@ocamlpro.com>"
 "José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>")

(maintainers "Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>")

(maintenance_intent
  "(latest).(latest).(any)"
  "(latest).(latest-1).(latest)"
  "(latest).(latest-2).(latest)"
  "(latest).(latest-3).(latest)"
  "(latest).(latest-4).(latest)")

(documentation "https://formalsec.github.io/smtml/smtml/index.html")

(package
 (name smtml)
 (synopsis "An SMT solver frontend for OCaml")
 (description
  "Smt.ml is an SMT solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability.")
 ; Optional solver dependencies
 ; Change here sould be mirrored in "conflicts"
 (depopts alt-ergo-lib bitwuzla-cxx colibri2 cvc5 z3)
 (conflicts
  (bitwuzla-cxx
   (< "0.6.0"))
  (alt-ergo-lib
   (< "2.6.2"))
  (z3
   (or
    (< "4.12.2")
    (>= "4.16"))))
 (depends
  bos
  (cmdliner
   (>= "1.3.0"))
  dune
  (dune-build-info
   (>= "3.20"))
  (dune-site
   (>= "3.20"))
  (dolmen
   (>= "0.10"))
  (dolmen_type
   (>= "0.10"))
  (dolmen_model
   (>= "0.10"))
  (fmt
   (>= "0.8.7"))
  fpath
  farith
  (hc
   (>= "0.5"))
  (menhir
   (and
    :build
    (>= "20220210")))
  (ocaml
   (>= "4.14.0"))
  ocaml_intrinsics
  ppx_deriving
  ppx_enumerate
  (prelude
   (>= "0.5"))
  rresult
  (scfg
   (>= "0.5"))
  (mtime
   (>= "2.0.0"))
  (yojson
   (>= "1.6.0"))
  (zarith
   (>= "1.5"))
  ;; Doc dependencies
  (odoc :with-doc)
  (sherlodoc :with-doc)
  ;; Test dependencies
  (ounit2 :with-test)
  (bisect_ppx
   (and
    :with-dev-setup
    (>= "2.5.0")))
  ;; Dev dependencies
  (ocamlformat
    (and
      (>= "0.29.0")
      :with-dev-setup))
  (ocaml-lsp-server :with-dev-setup)
  (benchpress
   (and
    :with-dev-setup
    (= "dev")))
  (cohttp :with-dev-setup)
  (cohttp-lwt-unix :with-dev-setup)
  (extunix :with-dev-setup)
  (dune-glob :with-dev-setup)
  (lwt :with-dev-setup)
  (mdx :with-test)
  (re :with-dev-setup)
  (sexplib :with-dev-setup)
  (tls-lwt :with-dev-setup))
 (sites (share data)))