this repo has no description
anil.recoil.org
1opam-version: "2.0"
2maintainer: "Maël Valais <mael.valais@gmail.com>"
3authors: ["Maël Valais <mael.valais@gmail.com>" "Olivier Lezaud"]
4homepage: "https://www.irit.fr/touist"
5bug-reports: "https://github.com/touist/touist/issues"
6license: "MIT"
7dev-repo: "git+https://github.com/touist/touist.git"
8build: [
9 [
10 "ocaml"
11 "setup.ml"
12 "-configure"
13 "--prefix"
14 prefix
15 "--%{yices2:enable}%-yices2"
16 "--%{qbf:enable}%-qbf"
17 ]
18 ["ocaml" "setup.ml" "-build"]
19 [
20 "ocaml"
21 "setup.ml"
22 "-configure"
23 "--enable-tests"
24 "--%{yices2:enable}%-yices2"
25 "--%{qbf:enable}%-qbf"
26 ] {with-test}
27 ["ocaml" "setup.ml" "-build"] {with-test}
28 ["ocaml" "setup.ml" "-test"] {with-test}
29 ["ocaml" "setup.ml" "-doc"] {with-doc}
30]
31install: ["ocaml" "setup.ml" "-install"]
32remove: [
33 "ocaml" "%{etc}%/touist/setup.ml" "-C" "%{etc}%/touist" "-uninstall"
34]
35depends: [
36 "ocaml" {>= "4.01.0" & < "5.0.0"}
37 "cppo" {build & >= "0.9.4"}
38 "cppo_ocamlbuild" {build}
39 "fileutils" {build & >= "0.4.0"}
40 "menhir" {build & >= "20151023"}
41 "minisat" {build & < "0.6"}
42 "ocamlbuild" {build}
43 "ocamlfind" {build}
44 "ounit" {with-test & < "2.2.6"}
45]
46depopts: ["qbf" "yices2"]
47conflicts: [
48 "qbf" {< "0.1"}
49 "yices2" {< "0.0.2"}
50]
51post-messages: [
52 "
53Touist built without yices2. If you also wanted to use the SMT solver, do:
54 opam install yices2
55 opam reinstall touist
56 "
57 {success & !yices2:installed}
58 "
59Touist built without quantor. If you also wanted to use the QBF solver, do
60 opam install qbf
61 opam reinstall touist
62 "
63 {success & !qbf:installed}
64 "
65Touist has been built with the yices2 solver. Yices2 is free [only] for
66non-commercial use. License terms:
67 http://yices.csl.sri.com/yices-newnewlicense.html
68 "
69 {success & yices2:installed}
70 "
71Touist has been built with the solver 'quantor'. Quantor is under BSD
72license.
73 "
74 {success & qbf:installed}
75]
76synopsis: "The solver for the Touist language"
77description: """
78The Touist language is a friendly language for writing propositional
79logic (SAT), logic on real and integers (SMT) and quantified boolean
80formulas (QBF). This language aims to formalize real-life problems
81(e.g., the sudoku can be solved in a few lines). Touist embeds a SAT
82solver (minisat) and can be built with optionnal SMT and QBF solvers.
83Touist is also able to generate the latex, DIMACS, SMT-LIB and QDIMACS
84formats from a touist file.
85
86Optionnal solvers:
87- for using the embeded SMT solver, run `opam install yices2` and then do
88 `opam reinstall touist`
89- for using the embeded QBF solver, run `opam install qbf` and then do
90 `opam reinstall touist`"""
91url {
92 src: "https://github.com/touist/touist/archive/v3.2.1.tar.gz"
93 checksum: [
94 "sha256=1085e30db117f0fe61bc506531964a6c5c007db9c7b52f166a5d5c9acae357ff"
95 "md5=b37b3aaefba542930f0e2b94cd0d79c1"
96 ]
97}