Provide binary download

[Timmmm]

A fairly common theme among Sail users is that it's a bit of a nightmare to install. Certainly for us I think every single one of my colleagues that tried to install it had issues with OPAM. The most ridiculous was that if you are in more than 32 groups it can't find curl. Yeah I'm not sure what kind of code you have to write to have a bug like that...

Anyway we "solved" this by caching the C model output, based on a hash of all the Sail files and the Sail command line and compiler version. It works very well for people that don't edit the Sail code - now they only dependencies they have are libgmp (pretty easy to install) and GCC.

It doesn't really help people that need to edit the Sail code though. I think something that might help is to provide precompiled Linux binaries as a .tar.gz that you can just download, unzip and add to your PATH. It could include Z3 too so you don't need to install that (we have to compile it from source on RHEL 8 annoyingly).

What do you think? I could have a go at setting it up if you like?

[Alasdair]

Yes, if you know the GitHub Action incantations to get it to output a tarball that would be very useful!

If we wanted to support ancient RHEL we might have to use a docker container, but I think you can do that in GH actions.

[PeterSewell]

I think all three might be useful - prebuilt binary of the C, tarball, and docker container. Maybe we should just provide all of them?

…

On Thu, 9 May 2024 at 01:24, Alasdair Armstrong ***@***.***> wrote: Yes, if you know the GitHub Action incantations to get it to output a tarball that would be very useful! If we wanted to support ancient RHEL we might have to use a docker container, but I think you can do that in GH actions. — Reply to this email directly, view it on GitHub <#532 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZVQHGYCAJU4YJFZWYTZBK62DAVCNFSM6AAAAABHNXN2XCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBRG4YDOOBTGY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Timmmm]

Yeah definitely. I think for the Docker container Alasdair was talking about using that to build Sail in CI so it only requires an ancient glibc. I think it's pretty much a one-line change for that fortunately, e.g. here's the solution in another project.

Anyway I will have a go at the binary tarballl of the compiler first. The prebuild C model is more of a pain (#534 would help a bit), but I think it's also less critical if you can easily download and install the Sail compiler.

[Timmmm]

Ok I've made some pretty good progress on this. See this commit. It does two things:

• Add a Makefile target and CI workflow to build Sail and Z3 on Rocky 8 and zip them up.
• Change the default SAIL_DIR / Manifest.dir so that instead of hard-coding it at opam install time, it calculates it at runtime relative to the sail binary. I.e. <sail binary dir>/../share/sail.

The second change makes the Sail install actually portable (relocatable?) without having to worry about opam var sail:share or SAIL_DIR at all (though you can still use SAIL_DIR if necessary). It works for the tarball download, and when installed by opam.

I think this is much nicer and simplifies this mess in the RISC-V Makefile:

There are a few things that aren't quite resolved:

1. I don't understand what EXPLICIT_COQ_SAIL in that Makefile is. Any idea?
2. For some reason sail --version comes out as Sail unknown (unknown @ unknown). Probably an easy fix; I haven't looked into it at all.
3. It seems like you have a workflow for running Sail from the source repo, without doing make install. I don't know what it is though so I'm not sure if I've broken it. How do you normally run Sail during development?

Anyway this seems like a good point to get feedback. The tarball (which Github helpfully zips) is here if you want to try it: https://github.com/Timmmm/sail/actions/runs/9037870387/artifacts/1492512434

[Alasdair]

Thanks, I'll take a look at your commit. I'll probably add your changes to https://github.com/Alasdair/sail/tree/sail2 and work on it there. I find using a personal fork is pretty useful to avoid spamming our mailing list when working with anything involving github actions.

I think the RISC-V Makefile was set up before I added the sail --dir flag, which is probably why it does things that way. For the version thing, it tries to pick up the version from either git or opam, so if you have neither it just doesn't know. I think we should just have an ocaml file that does something like let version = { major = X; minor = Y; patch = Z } and remove all that logic entirely. This will also simplify the --require-version flag we wanted.

Change the default SAIL_DIR / Manifest.dir so that instead of hard-coding it at opam install time, it calculates it at runtime relative to the sail binary. I.e. /../share/sail

If we strip out the version logic from manifest.ml, we might be able to replace the little program that generates it with just a (copy_files ...) stanza in the dune, and then the logic would be either do the existing opam thing, or be relative to the binary when not installed via opam - I'm not sure we can 100% rely on opam always putting the same things in the same places on every platform.

I normally just do make install, but I think the script in the root should still work

[Alasdair]

I could also look at getting a web server where we could push builds - I'm not sure the github releases page would work if we wanted to do anything like nightly builds.

[Timmmm]

For the version thing, it tries to pick up the version from either git or opam, so if you have neither it just doesn't know.

Yeah that's what I don't quite get though - it works when I build it locally, and I'm pretty sure Github CI does actually clone the repo. Weird.

I think we should just have an ocaml file that does something like let version = { major = X; minor = Y; patch = Z } and remove all that logic entirely. This will also simplify the --require-version flag we wanted.

I definitely agree. Is the change in #497 ok? Wasn't sure if you wanted more changes in it, or to do it in a different way? It doesn't get rid of the branch/hash parts but it does hard-code the version.

I'm not sure the github releases page would work if we wanted to do anything like nightly builds.

You can do automatic uploads to github releases. It is a bit of a pain, but maybe less pain than setting up a separate web server with authentication and all that.

[bacam]

1. I don't understand what `EXPLICIT_COQ_SAIL` in that Makefile is. Any idea?

It's to indicate whether additional flags are necessary to find the Coq Sail library when building Coq output. It's also out of date because the Coq Sail library isn't in the main repository any more, so you can safely remove that particular line. I intend to rebase the pull request I have open to update the Coq support for the RISC-V model anyway, so I'll fix it to up to find the library properly then.

[Timmmm]

Ok I managed to figure out how to make git describe work, so this download works:

❯ bin/sail --version
Sail 0.17.1 (binary_release @ f4050fdb682d72e7671049c2bd65c9a270347b29)

I'm not sure we can 100% rely on opam always putting the same things in the same places on every platform.

Perhaps this is ok because you can still use SAIL_DIR if it's wrong, like you have to already? Also the initial binary is only for Linux so maybe we can cross that bridge when it on Mac comes to it. (Having tried to install OCaml on Windows I seriously doubt anyone is going to be doing that...)

I'll make a PR anyway and we can continue the discussion there.

[Alasdair]

I think OCaml windows support has been improving quite a bit recently so it's not impossible that somebody might try