Skip to content

Commit

Permalink
[new release] sail_smt_backend, sail_output, sail_ocaml_backend, sail…
Browse files Browse the repository at this point in the history 
…_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: rems-project/sail#203
* Issue 202: rems-project/sail#202
* Issue 188: rems-project/sail#188
* Issue 187: rems-project/sail#187
* Issue 277: rems-project/sail#277

Various mapping issues such as:

* Issue 244: rems-project/sail#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.
  • Loading branch information
@Alasdair
Alasdair committed Aug 25, 2023
1 parent 47a1176 commit 559b499
Show file tree
Hide file tree
Showing 11 changed files with 584 additions and 0 deletions.
69 changes: 69 additions & 0 deletions packages/libsail/libsail.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
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 changes: 71 additions & 0 deletions packages/sail/sail.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
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 changes: 49 additions & 0 deletions packages/sail_c_backend/sail_c_backend.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
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 changes: 49 additions & 0 deletions packages/sail_coq_backend/sail_coq_backend.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
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 changes: 51 additions & 0 deletions packages/sail_doc_backend/sail_doc_backend.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
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 changes: 50 additions & 0 deletions packages/sail_latex_backend/sail_latex_backend.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
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 changes: 49 additions & 0 deletions packages/sail_lem_backend/sail_lem_backend.0.16/opam
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
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"
Loading

0 comments on commit 559b499

Please sign in to comment.