PeterSewell
commented
2 years ago Hi Andrew,
we did think about that, but IIRC it was deemed by the opam experts in the group to not be idiomatic to provide the generated theorem-prover definitions as opam packages. Instead, we provide snapshots of the prover-generated models in the model github repos, eg for Armv8.5-A at https://github.com/rems-project/sail-arm/tree/master/arm-v8.5-a/snapshots and RISC-V at https://github.com/riscv/sail-riscv/tree/master/prover_snapshots
best, Peter
On Fri, 29 Oct 2021 at 13:59, Andrew Appel @.***> wrote:
Has the sailing team considered providing opam packages for users of specific ISA descriptions in Coq? Such a user may want to just include a (prebuilt) opam package for the ARM or x86_64 or whatever, rather than installing Sail itself and building everything.
Perhaps this is a naive question; I'm not an opam expert and perhaps there's a way to specify within opam, "install this opam package of Sail itself, then run sail on that architecture description, then turn that into an opam package, then load that package"; but I'm guessing no.
My point is, Sail is not the only product here, some of your output artifacts (Coq formalizations built from well-researched Sail descriptions of real ISAs) could now be considered products, and you could support opam releases of those. That would make those things much easier to import into Coq developments of compilers, static analyzers, circuit designs, etc. that would rely on them.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/157, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZWDB47423IWLI5EJBTUJKLDLANCNFSM5G7I3AWQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.
Has the sailing team considered providing opam packages for users of specific ISA descriptions in Coq? Such a user may want to just include a (prebuilt) opam package for the ARM or x86_64 or whatever, rather than installing Sail itself and building everything.
Perhaps this is a naive question; I'm not an opam expert and perhaps there's a way to specify within opam, "install this opam package of Sail itself, then run sail on that architecture description, then turn that into an opam package, then load that package"; but I'm guessing no.
My point is, Sail is not the only product here, some of your output artifacts (Coq formalizations built from well-researched Sail descriptions of real ISAs) could now be considered products, and you could support opam releases of those. That would make those things much easier to import into Coq developments of compilers, static analyzers, circuit designs, etc. that would rely on them.