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: "http://touist.github.io"
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}
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, 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 the
82minisat solver (for propositional logic) and the yices2 solver
83(optional, for SMT logic). It can also generate the DIMACS, SMT2 and
84latex formats from you 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.0.tar.gz"
93 checksum: [
94 "sha256=15ecbaa2ee1dc111a383047b1daf15f93121ad42d3f521c2f89e0e8d37f71e79"
95 "md5=42be6b20683d4b19d3e0379bb0dd846e"
96 ]
97}