[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#1065419: marked as done (ITP: sail-ocaml -- Sail architecture definition language)

Your message dated Thu, 07 Aug 2025 15:00:21 +0000
with message-id <E1uk26P-00Cd2u-0V@fasolo.debian.org>
and subject line Bug#1065419: fixed in sail-ocaml 0.19.1+dfsg5-1
has caused the Debian Bug report #1065419,
regarding ITP: sail-ocaml -- Sail architecture definition language
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
1065419: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065419
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: wnpp
Severity: wishlist
Owner: Bo YU <tsu.yubo@gmail.com>
X-Debbugs-Cc: debian-devel@lists.debian.org

* Package name    : sail-ocaml
  Version         : 0.17.1
  Upstream Contact: rems-project 
* URL             : https://github.com/rems-project/sail
* License         : BSD-2-Clause
  Programming Lang: OCaml 
  Description     : Sail architecture definition language with OCaml

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.

Given a Sail definition, the tool will type-check it and generate documentation, executable emulators (in C and OCaml), theorem-prover definitions (for Isabelle, HOL4, and Coq), and definitions to integrate with our RMEM and isla-axiomatic tools for concurrency semantics. The Isla engine provides SMT-based symbolic evaluation for Sail models, and the Islaris verification tool integrates Isla output with the Iris program logic to support proof about binary code in Coq. Not all models are integrated with all tools - see the most recent papers and models for descriptions of the current state.

------------>>>----------
This is a denpendency of sail-riscv[0] and I will maintain it under
Debian OCaml team.

[0]: https://github.com/riscv/sail-riscv
-- 
Regards,
--
  Bo YU

Attachment: signature.asc
Description: PGP signature


--- End Message ---
--- Begin Message --- 
Source: sail-ocaml
Source-Version: 0.19.1+dfsg5-1
Done: Bo YU <vimer@debian.org>

We believe that the bug you reported is fixed in the latest version of
sail-ocaml, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1065419@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Bo YU <vimer@debian.org> (supplier of updated sail-ocaml package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 1.8
Date: Tue, 10 Jun 2025 17:36:25 +0800
Source: sail-ocaml
Binary: libsail-ocaml-dev libsail-ocaml-dev-dbgsym sail-ocaml sail-ocaml-dbgsym
Architecture: source amd64
Version: 0.19.1+dfsg5-1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Bo YU <vimer@debian.org>
Description:
 libsail-ocaml-dev - language describes the instruction semantics of processors
 sail-ocaml - language describes the instruction semantics of processors
Closes: 1065419
Changes:
 sail-ocaml (0.19.1+dfsg5-1) unstable; urgency=medium
 .
   * Initial release. (Closes: #1065419)
Checksums-Sha1:
 25129af8e58a3094ed427cc7df015f5b18febb7d 2935 sail-ocaml_0.19.1+dfsg5-1.dsc
 7e41f2918ff503b0a506ca3da36a6c3d4cc19271 1150144 sail-ocaml_0.19.1+dfsg5.orig.tar.xz
 c4b0dabc0e2a967308ea21b65200fe4051904550 5992 sail-ocaml_0.19.1+dfsg5-1.debian.tar.xz
 9f69a2c791416a5f6da341c5349235e5e21c4e2a 1022196 libsail-ocaml-dev-dbgsym_0.19.1+dfsg5-1_amd64.deb
 621edbc6a3cf1454ee1bdd5b20b378054fa502e8 35652920 libsail-ocaml-dev_0.19.1+dfsg5-1_amd64.deb
 ed79a22e03ca975e08e241693e2130c7cf71646e 1247996 sail-ocaml-dbgsym_0.19.1+dfsg5-1_amd64.deb
 c14c5979fab0fdda521b50acad7c2eb781a4772c 8543 sail-ocaml_0.19.1+dfsg5-1_amd64.buildinfo
 6b9c8dff1f9626b049b9b065a4a4e68349c7cef2 4077120 sail-ocaml_0.19.1+dfsg5-1_amd64.deb
Checksums-Sha256:
 2e8557d391e074177e818e062cfdab501232602940de079fd9795d720c3b767d 2935 sail-ocaml_0.19.1+dfsg5-1.dsc
 7dd7444582c66719e05eea99ebd72dd01733351eb1a00f1cb5a79fb0001a034b 1150144 sail-ocaml_0.19.1+dfsg5.orig.tar.xz
 71eddd05d84b8aae36a2bda1e24eb31f9c6aa0ed9cf206bd20a724ff4bfaf2a9 5992 sail-ocaml_0.19.1+dfsg5-1.debian.tar.xz
 62ad5a330f473c8e38e7d5f7fc76e5a00f29c069120d0016a179db690eb30d83 1022196 libsail-ocaml-dev-dbgsym_0.19.1+dfsg5-1_amd64.deb
 ca48b50e234fa8292c71ae8219e447b482fdeb261c8a82376a952889de7a1f08 35652920 libsail-ocaml-dev_0.19.1+dfsg5-1_amd64.deb
 df4253a3b9686ae78985687d351762287585b288cc0a052326c1f3910ab645e4 1247996 sail-ocaml-dbgsym_0.19.1+dfsg5-1_amd64.deb
 6f2aa0d98405ba3f55ed6210174fcb6c98e17822fe19ff1baf6e1db7d114d177 8543 sail-ocaml_0.19.1+dfsg5-1_amd64.buildinfo
 d8d1fd4b30d2ede5234e233b8227036f13198096f2126bfdcdecd86b924357d1 4077120 sail-ocaml_0.19.1+dfsg5-1_amd64.deb
Files:
 5fe2ad289bc19e5fc771872b0b99789f 2935 ocaml optional sail-ocaml_0.19.1+dfsg5-1.dsc
 7c4d3937b37ec4fbe20b05490ec7388e 1150144 ocaml optional sail-ocaml_0.19.1+dfsg5.orig.tar.xz
 1afaf34e874fb2dc0f454388ff729742 5992 ocaml optional sail-ocaml_0.19.1+dfsg5-1.debian.tar.xz
 732901fea343870dd6b9b01eb7d5ee8d 1022196 debug optional libsail-ocaml-dev-dbgsym_0.19.1+dfsg5-1_amd64.deb
 027258d0b5dfb1732af476d9605cc0c9 35652920 ocaml optional libsail-ocaml-dev_0.19.1+dfsg5-1_amd64.deb
 8163576294f9138045223864bc2d9d65 1247996 debug optional sail-ocaml-dbgsym_0.19.1+dfsg5-1_amd64.deb
 37ffa994385eb39089f53041784201cf 8543 ocaml optional sail-ocaml_0.19.1+dfsg5-1_amd64.buildinfo
 261b40f239386c576b662de06c511721 4077120 ocaml optional sail-ocaml_0.19.1+dfsg5-1_amd64.deb

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEIcmhjYVTlmab0tjp+RVP3hQ+S68FAmiGRBsACgkQ+RVP3hQ+
S68FBw/6ArSvgkNmSz7oIzT02vHKTQerPoyKGxPAWffD6IG37oluVGwiRcV4SqFV
78q8GLgR1dB2aRJLwSDBIS151ni1bBsJCrcMTodxLxZzYgVkjjA5BefUOzAd6nnW
K7obP/Jru0mhzLgTvVs7ufpbZ0TEIarlTVHfvl20m+3FxJLxyGVJ3BSIjrse3pP/
zcvOsKGuB4liSXa058RSO7P1Wwqns2loQ1yDjDu1j5BZgoXgc73q1a4pCHaX3yOa
ZG9f8bHubEBXSjRrWVVqIyBPT45RTc0s3BGrWv7tktT26WN1lsCs1wkAIDkuDvHW
TbgvKWATb5CgU9BcOMpl12dnT0KQXuMoG3Y463F62J1udyzTua4KoDce6am8N4Ru
VMXSkuQrRiw43xLCUhDF5+nWtrkaFZYVY+OrpVc7HNOXMUnc0wnijqj8EsORSA8+
pnNIDPzXXto3tiTFxJ9HwDVXtB4iacuyQbeieWgZaFg4tGV9kTdz6w8gbjTBO2xK
PEMwuxsI0s6bEujgvU/DEbNVisyWicRMTWhr/vIyh42R2uqare7qgWUnG/YzjZvb
Df662TAiLhxWwFI//vNhp07QIgrCbPvpYlJtZpr0CMEcNKBhXzkLwjey5f1FTRu9
0ZlQDVUfIVQBdVt3hZ2jVf5e6thPoHgt6wOyz7QvtrTAiZeap0w=
=6TPP
-----END PGP SIGNATURE-----

Attachment: pgpchDRqnyr57.pgp
Description: PGP signature


--- End Message ---
Reply to: