[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: 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.
nberth · May 16, 2024 · 71008d6 · 71008d6
1 parent 87dbf4d
commit 71008d6
Show file tree

Hide file tree

Showing 11 changed files with 584 additions and 0 deletions.
diff --git a/packages/libsail/libsail.0.16/opam b/packages/libsail/libsail.0.16/opam
@@ -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"
diff --git a/packages/sail/sail.0.16/opam b/packages/sail/sail.0.16/opam
@@ -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"
diff --git a/packages/sail_c_backend/sail_c_backend.0.16/opam b/packages/sail_c_backend/sail_c_backend.0.16/opam
@@ -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"
diff --git a/packages/sail_coq_backend/sail_coq_backend.0.16/opam b/packages/sail_coq_backend/sail_coq_backend.0.16/opam
@@ -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"
diff --git a/packages/sail_doc_backend/sail_doc_backend.0.16/opam b/packages/sail_doc_backend/sail_doc_backend.0.16/opam
@@ -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"
diff --git a/packages/sail_latex_backend/sail_latex_backend.0.16/opam b/packages/sail_latex_backend/sail_latex_backend.0.16/opam
@@ -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"
diff --git a/packages/sail_lem_backend/sail_lem_backend.0.16/opam b/packages/sail_lem_backend/sail_lem_backend.0.16/opam
@@ -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"