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
146
147
148
149
150
151
152
153
|
(lang dune 3.0)
(using menhir 2.1)
(using dune_site 0.1)
(name sail)
(version 0.19.1)
(generate_opam_files true)
(wrapped_executables false)
(source
(github rems-project/sail))
(maintainers "Sail Devs <cl-sail-dev@lists.cam.ac.uk>")
(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)
(depends
(ocaml (>= 4.08.1))))
(package
(sites (lib 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 (>= 20240715) :build))
(ott (and (>= 0.28) :build))
(lem (>= "2018-12-14"))
(linksem (>= "0.3"))
conf-gmp
(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 SMT 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_lean_backend)
(synopsis "Sail to Lean 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_lean_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))))
|
