forked from rems-project/sail
-
Notifications
You must be signed in to change notification settings - Fork 0
/
dune-project
145 lines (125 loc) · 3.69 KB
/
dune-project
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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
(lang dune 3.0)
(using menhir 2.1)
(using dune_site 0.1)
(name sail)
(version 0.17)
(generate_opam_files true)
(wrapped_executables false)
(source
(github rems-project/sail))
(maintainers "Sail Devs <[email protected]>")
(license BSD-2-Clause)
(authors
"Alasdair Armstrong"
"Thomas Bauereiss"
"Brian Campbell"
"Shaked Flur"
"Jonathan French"
"Kathy Gray"
"Robert Norton"
"Christopher Pulte"
"Peter Sewell"
"Mark Wassell")
(package
(synopsis "Helper tool for compiling Sail")
(name sail_manifest))
(package
(sites (share plugins))
(name libsail)
(synopsis "Sail is a language for describing the instruction semantics of processors")
(description "\
Sail is a language for describing the instruction-set
architecture (ISA) semantics of processors. Sail aims to provide a
engineer-friendly, vendor-pseudocode-like language for describing
instruction semantics. It is essentially a first-order imperative
language, but with lightweight dependent typing for numeric types and
bitvector lengths, which are automatically checked using Z3. It has
been used for several papers, available from
http://www.cl.cam.ac.uk/~pes20/sail/.
")
(depends
(dune-site (>= 3.0.2))
(bisect_ppx (and :dev (>= "2.5.0")))
(menhir (and (>= 20180523) :build))
(ott (and (>= 0.28) :build))
(lem (>= "2018-12-14"))
(linksem (>= "0.3"))
conf-gmp
conf-zlib
(yojson (>= 1.6.0))
(pprint (>= 20220103))))
(package
(name sail_ocaml_backend)
(synopsis "Sail to OCaml translation")
(depends
(libsail (= :version))
(base64 (>= 3.1.0))))
(package
(name sail_c_backend)
(synopsis "Sail to C translation")
(depends
(libsail (= :version))))
(package
(name sail_smt_backend)
(synopsis "Sail to C translation")
(depends
(libsail (= :version))))
(package
(name sail_sv_backend)
(synopsis "Sail to Systemverilog translation")
(depends
(libsail (= :version))))
(package
(name sail_lem_backend)
(synopsis "Sail to Lem translation")
(depends
(libsail (= :version))))
(package
(name sail_coq_backend)
(synopsis "Sail to Coq translation")
(depends
(libsail (= :version))))
(package
(name sail_output)
(synopsis "Example Sail output plugin")
(depends
(libsail (= :version))))
(package
(name sail_latex_backend)
(synopsis "Sail to LaTeX formatting")
(depends
(libsail (= :version))
(omd (and (>= 1.3.1) (< 1.4.0)))))
(package
(name sail_doc_backend)
(synopsis "Sail documentation generator")
(depends
(libsail (= :version))
(base64 (>= 3.1.0))
(omd (and (>= 1.3.1) (< 1.4.0)))))
(package
(name sail)
(synopsis "Sail is a language for describing the instruction semantics of processors")
(description "\
Sail is a language for describing the instruction-set
architecture (ISA) semantics of processors. Sail aims to provide a
engineer-friendly, vendor-pseudocode-like language for describing
instruction semantics. It is essentially a first-order imperative
language, but with lightweight dependent typing for numeric types and
bitvector lengths, which are automatically checked using Z3. It has
been used for several papers, available from
http://www.cl.cam.ac.uk/~pes20/sail/.
")
(depends
(libsail (= :version))
(sail_manifest (and (= :version) :build))
(sail_ocaml_backend (and (= :version) :post))
(sail_c_backend (and (= :version) :post))
(sail_smt_backend (and (= :version) :post))
(sail_sv_backend (and (= :version) :post))
(sail_lem_backend (and (= :version) :post))
(sail_coq_backend (and (= :version) :post))
(sail_latex_backend (and (= :version) :post))
(sail_doc_backend (and (= :version) :post))
(sail_output (and (= :version) :post))
(linenoise (>= 1.1.0))))