Continuous build of Z3 docker images

[dee-me-tree-or-love]

It's my first issue here, so I'm sorry in advance if anything's off in the description, please feel free to correct me :)

Hello everyone!

I've been using Z3 recently for study purposes and during that time found it very convenient to run the tool from a docker container. However, I couldn't find a readily available image that would be exactly up to date with the Z3 repo, so I've made a fork that continuously builds the image and pushes it to docker repo under z3-fork name. I've based the work on top of the available Dockerfile's that are already included in the repository's contrib/ci/dockerfiles directory and only added a few github action yamls.

Currently, the fork images are built weekly (every Sunday night), and are tagged, for example, like this: z3-fork:ubuntu-20.04-bare-z3-edge (based on the latest commit on main branch) and z3-fork:ubuntu-20.04-bare-z3-20211219 (indicating the build date).

I'd like to ask if anyone thinks that this might be useful? Then I'd be more than happy to open a PR from my work to add the github action files ✌️ (and if it doesn't seem too relevant, I of course understand and won't take any offense.)

Changed files

Added:

• .github/workflows/publish-docker.yml to manage GitHub Actions.
• docker/ubuntu-20-04.Dockerfile as a simplified version of the original Dockerfile.

Example usage

# create a file in, say, examples/task1.smt2
$ cat ./examples/task1.smt2

(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
(check-sat)

# -i flag allows to connect to standard input
$ cat examples/task1.smt2 | docker run --rm -i deemetree/z3-fork:ubuntu-20.04-bare-z3-edge -in -smt2

sat

Will be happy to hear if that's of any use. Sorry again if I'm submitting the issue in any wrong form.

[NikolajBjorner]

that would be very sweet, yes please add pull request or allow to integrate it.

[NikolajBjorner]

The main issue may be around managing dockerhub access. I am not tuned into what process is available to Microsoft projects. There is some process for sure, but it would require some bandwidth to establish credentials and end-points.
To start with I added your action and docker file to the repository. It will not do much until the end-point question is resolved.

[NikolajBjorner]

Take a look at
https://github.com/Z3Prover/z3/blob/NikolajBjorner-ghcr/.github/workflows/docker-image.yml
It attempts to push to ghcr so requires some other magic than your script.
Mostly it seems to be about adding a registry reference, but I am not at all familiar with deploying to CRs.
If you can assist in getting this to work, then we can build on this action to generate and host suitable images.

[NikolajBjorner]

The docker is now publicly available. https://github.com/z3prover/z3/pkgs/container/z3

[NikolajBjorner]

it is converted to a discussion because the updates could be endless and not associated with a particular issue.
Please add pull requests with feature adds (python/etc).

[dee-me-tree-or-love]

Hello @NikolajBjorner, thank you so much for reacting and picking this issue up. My apologies for the lack of activity in the meantime, unfortunately I was kept busy by a few other projects at the time. I will try to revisit this discussion and the idea I had at that time and will be happy to assist if that is still applicable. These days I am still ending up quite busy and unfortunately cannot promise a fast contribution, but I will do as much as possible. Thanks once again for considering this!