Add Docker image and continuous deployment for it

[Niols]

closes #217

This PR defines a Docker image with just enough to run Rosette with Z3. It also adds a GitHub workflow to automatically build the Docker image on pushes to main and pull requests and to automatically publish the Docker image to GitHub Packages.

In general, I believe the Docker image is quite well documented. A lot of things have also been discussed in #217. For the base image, the choice was to work from scratch, building on top of Alpine and installing Racket by hand. It should be fairly easy to update the Dockerfile for another version of Racket.

The Docker image has a bit of a complicated structure:

• It first imports only the info.rkt files and uses them to install all of Rosette's dependencies. (The trick that I use for that seems fairly complicated: if you have a better solution, I'd love to hear it!)
• Once this is done, it imports all the files of the current directory and builds and installs Rosette.

The reason for this structure is to make the best use of Docker's cache: as long as info.rkt do not change, rebuilding the Docker image is only a matter of rebuilding Rosette. (On my laptop, around 45 seconds.) This can be practical when developing locally with Rosette. It also speeds up the continuous deployment when there has been a build less than seven (ten?) days before.

The Docker image presents a user rosette in group rosette, working in /rosette by default. It is fairly easy to make Rosette work on external files by use of mounting, eg. with:

time docker run --mount type=bind,source="$PWD",target=/src ghcr.io/emina/rosette /src/test.rkt

while having an appropriate test.rkt file in the current directory. You may actually try the above command with ghcr.io/niols/rosette:docker-demo which I published for demonstration purposes and will remove after this PR is done. This will require you to login to GHCR as shown here, you might want a PAT with no specific rights for that.

The Docker image does not contain documentation of Rosette or its dependencies, so as to reduce its size. If you knew how I could also remove build dependencies, that would be great. The Docker image is also built on top of Racket minimal and does not include what is necessary to run DrRacket. I didn't think it was the goal but if I am mistaken please let me know and I will fix it.

I took the liberty to add a configuration for Dependabot, that creates pull requests whenever GitHub Action dependencies can be updated (eg. action/checkout).

In order to work properly, the GitHub Action workflow needs to be able to push to GitHub Packages. This can be done in the global Settings > Developer Settings > Personal access tokens, by creating a new token that has the write:packages rights (which will imply the repo rights). This token then has to be provided as a secret in the repository's Settings > Secrets > Actions under the name BOT_PAT. I can rename this in something else if you think that is more appropriate, eg. GHCR_PAT?

We could easily adapt this PR to publish to Docker Hub instead, which would avoid requiring people to login to GitHub Packages and have the image be named emina/rosette instead of ghcr.io/emina/rosette.

I probably forgot a lot of things, so don't hesitate to shoot if you have questions!

[lukenels]

This looks great to me! I've added a couple of minor comments to this review. I'll do some more testing and sync up with @emina to generate the tokens. Will we be able to test the GitHub Action Docker build/push workflow in response to this PR before merging it in to master?

[lukenels]

It seems that the personal access token BOT_PAT is only used to clone the repository. Why is that necessary if the repository is public? Could we get away without creating a personal access token and just using the GITHUB_TOKEN to build/push the Docker image?

[jamesbornholt]

Thanks for doing this, it's super awesome and automates a task I've done by hand many times before :-)

[Niols]

A lot of great comments. Let me integrate all of this!

[Niols]

Following @lukenels's suggestion, the entry point is now /usr/bin/racket -I rosette. This can in particular be used to jump in a REPL with:

docker run -it ghcr.io/emina/rosette

However, as of now, the REPL starts with:

Welcome to Racket v8.4 [cs].
; Warning: no readline support (ffi-lib: could not load foreign library
  path: libedit.so.3
  system error: Error loading shared library libedit.so.3: No such file or directory)

before working fine (but without readline). I tried fixing it quickly with apk add libedit but I'm not sure it provides the right version because I then get other errors. I can look into it if you think that's useful.

[Niols]

I haven't been successful fixing this readline issue within Alpine because libedit.so.3 does not seem to be provided by any package. I did manage on a Debian image (either based on Jack Firth's images or based on debian:stable-slim, installing Racket by hand) because the package libedit2 does provide exactly this.

[Niols]

Alright, I fixed the REPL. Somehow, there was a big inconsistency problem between libedit and Racket 8.4. This was not specific to Alpine but was also the case on Jack Firth's images. Downgrading to Racket 8.3 and installing libedit did the trick. You can give it a try a spawn a Racket+Rosette REPL with:

docker run -it ghcr.io/niols/rosette:docker-demo

(Later, of course, this will be possible with simply ghcr.io/emina/rosette.)

Should I propose a modification of the README to mention the Docker image or are we happy with keeping it a little bit more discrete? (It will still show up on the left panel in the packages section, unless you hide this section from the repository.)

[lukenels]

I don't think the libedit issue is that important—the REPL is not the most useful part of the image and it still works without libedit, just with less functionality. I think we would rather stick with version 8.4 of Racket for the image.

Let's hold off on README changes for now so we can do some end-to-end tests once this commit has landed and caused the image to be pushed to GitHub.

[Niols]

Alright. I just removed my last commit, then. It is still available on my fork in branch docker-libedit. What do we think of the current state?

[sorawee]

Racket 8.4 switches to use Chez Scheme's expeditor instead of libedit / readline. My very wild guess is that it couldn't find the necessary library for building expeditor (ncurses in particular), so it falls back to readline / libedit, but since Racket no longer uses readline by default, something's gone wrong.

[Niols]

Do you think we should fix the image by installing the appropriate dependencies (eg. ncurses)? Or should we leave the Dockerfile as-is for now (there is a warning but even the REPL is usable) and wait for another change in Racket's behaviour there?

[Niols]

My tests seem to suggest that you were very right @sorawee: the problem can be fixed by installing the ncurses system dependency and the expeditor-lib Racket dependency. This brings the size of the image up from 828MB to 829MB and one gets a fancy REPL with colours and history etc. This is really not much so I took the liberty to implement it in 1638b75. I can of course revert that commit again if we don't think that it is necessary. As always, you can try it with: docker run -it ghcr.io/niols/rosette.

[sorawee]

Ah, nice! I think this is better, especially if it only incurs not too much space, so this is better, I believe.

[jamesbornholt]

This is awesome:

$ wget -q https://gist.githubusercontent.com/jamesbornholt/b51339fb8b348b53bfe8a5c66af66efe/raw/54253ebc11faf464d6a3e951b7abf25f621a5dd7/synthesis.rkt
$ sudo docker run --mount type=bind,source="$PWD",target=/src ghcr.io/jamesbornholt/rosette:master /src/synthesis.rkt
(model
 [y -5])
(unsat)
52
(* (+ 2 y) (+ 2 y))
(model
 [y 3])
(model
 [x 6]
 [c 2])
(model
 [c 2])
(plus (plus 0 0) (mul x 10))

@lukenels is the expert here so I'll let him comment before merging, but this looks good to me!

[lukenels]

This looks great to me! The checks just finished running on the latest commit, so I'll go ahead and merge it now. If everything goes well it should publish the image to ghcr shortly 😄

[Niols]

https://github.com/emina/rosette/pkgs/container/rosette 🎉