this repo has no description

[new release] sail_smt_backend, sail_output, sail_ocaml_backend, sail_manifest, sail_lem_backend, sail_latex_backend, sail_doc_backend, sail_coq_backend, sail_c_backend, sail and libsail (0.16)

CHANGES:

##### New documentation backend

A new documentation backend for integrating with Asciidoctor has been
added.

##### Automatic formatting (EXPERIMENTAL)

The `sail -fmt` option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.

##### Fixes

Various bugfixes including:

* Issue 203: https://github.com/rems-project/sail/issues/203
* Issue 202: https://github.com/rems-project/sail/issues/202
* Issue 188: https://github.com/rems-project/sail/issues/188
* Issue 187: https://github.com/rems-project/sail/issues/187
* Issue 277: https://github.com/rems-project/sail/issues/277

Various mapping issues such as:

* Issue 244: https://github.com/rems-project/sail/issues/244

As well as other minor issues

The `val cast` syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.

The pattern completeness checker has been improved and is now context
sensitive in some cases.

Alasdair 559b4995 47a1176c

Changed files
+584
packages
libsail
libsail.0.16
sail
sail.0.16
sail_c_backend
sail_c_backend.0.16
sail_coq_backend
sail_coq_backend.0.16
sail_doc_backend
sail_doc_backend.0.16
sail_latex_backend
sail_latex_backend.0.16
sail_lem_backend
sail_lem_backend.0.16
sail_manifest
sail_manifest.0.16
sail_ocaml_backend
sail_ocaml_backend.0.16
sail_output
sail_output.0.16
sail_smt_backend
sail_smt_backend.0.16
+69
packages/libsail/libsail.0.16/opam
···
+
opam-version: "2.0"
+
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/.
+
"""
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"dune-site" {>= "3.0.2"}
+
"bisect_ppx" {dev & >= "2.5.0"}
+
"menhir" {>= "20180523" & build}
+
"ott" {>= "0.28" & build}
+
"lem" {>= "2018-12-14"}
+
"linksem" {>= "0.3"}
+
"conf-gmp"
+
"conf-zlib"
+
"yojson" {>= "1.6.0"}
+
"pprint"
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+71
packages/sail/sail.0.16/opam
···
+
opam-version: "2.0"
+
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/.
+
"""
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"sail_manifest" {= version & build}
+
"sail_ocaml_backend" {= version & post}
+
"sail_c_backend" {= version & post}
+
"sail_smt_backend" {= version & post}
+
"sail_lem_backend" {= version & post}
+
"sail_coq_backend" {= version & post}
+
"sail_latex_backend" {= version & post}
+
"sail_doc_backend" {= version & post}
+
"sail_output" {= version & post}
+
"linenoise" {>= "1.1.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
substs: [ "src/bin/manifest.ml" ]
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+49
packages/sail_c_backend/sail_c_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to C translation"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+49
packages/sail_coq_backend/sail_coq_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to Coq translation"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+51
packages/sail_doc_backend/sail_doc_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail documentation generator"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"base64" {>= "3.1.0"}
+
"omd" {>= "1.3.1" & < "1.4.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+50
packages/sail_latex_backend/sail_latex_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to LaTeX formatting"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"omd" {>= "1.3.1" & < "1.4.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+49
packages/sail_lem_backend/sail_lem_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to Lem translation"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+48
packages/sail_manifest/sail_manifest.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Helper tool for compiling Sail"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+50
packages/sail_ocaml_backend/sail_ocaml_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to OCaml translation"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"base64" {>= "3.1.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+49
packages/sail_output/sail_output.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Example Sail output plugin"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"
+49
packages/sail_smt_backend/sail_smt_backend.0.16/opam
···
+
opam-version: "2.0"
+
synopsis: "Sail to C translation"
+
maintainer: ["Sail Devs <cl-sail-dev@lists.cam.ac.uk>"]
+
authors: [
+
"Alasdair Armstrong"
+
"Thomas Bauereiss"
+
"Brian Campbell"
+
"Shaked Flur"
+
"Jonathan French"
+
"Kathy Gray"
+
"Robert Norton"
+
"Christopher Pulte"
+
"Peter Sewell"
+
"Mark Wassell"
+
]
+
license: "BSD-2-Clause"
+
homepage: "https://github.com/rems-project/sail"
+
bug-reports: "https://github.com/rems-project/sail/issues"
+
depends: [
+
"dune" {>= "3.0"}
+
"libsail" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/rems-project/sail.git"
+
url {
+
src:
+
"https://github.com/rems-project/sail/releases/download/0.16/sail-0.16.tbz"
+
checksum: [
+
"sha256=aa38dbc4236fe8f63a3eede7d8a097adc2bb0992e2198a782ffe339c767e1008"
+
"sha512=1c7279cb6db7c01a32ceedce6328886966eee46c25e552a2e69d2f5d201bd98b68c9d409e7a9233a709a09f4895c68b06df985833f6f60c2f201880a74a9e82c"
+
]
+
}
+
x-commit-hash: "393de35eba02f4b2a47e0d3798c90bf44a26da55"