aya-prover/aya-dev

Container image for Aya

WojciechKarpiel opened this issue · 5 comments

WojciechKarpiel commented

Proposal

Publish container images for Aya.

Rationale

Make running Aya more convenient, especially for first-time users.

This is largely about personal preference:
some people (myself included), when about to try out a new program,
are more inclined to execute docker run ... than to download a binary from the Internet.

Pros

  • Allow one-liner quickstart: docker run ...
  • Make container nerds happy

Cons

  • Proof assistants by nature do a lot of file system I/O. Containers by nature isolate filesystems. You can mount your filesystem into the container, but this is handled differently by different runtimes (container-root is host-root vs container-root is host-user). What I'm saying is: if you use containers but you don't want isolation then you get yourself in unnecessary trouble.
  • It's yet another thing to maintain
WojciechKarpiel commented

NVM, figured out that "discussion" is a Github feature, and not just another word for "talking".
Sorry for breaking the contributing guidelines, closing this issue

  • ❤️1
ice1000 commented

This is totally okay! How would I publish a docker container and how can I turn a bunch of CLI commands to install Aya into a docker container?

WojciechKarpiel commented

Aya uses JLink, so I think the easiest way is just to copy the generated JVM runtime into the image.
It'd look like below:

  1. Prepare a Containerfile (AKA Dockerfile), e.g.

    FROM docker.io/library/gradle:8-jdk21 as builder
COPY . /aya-dev
WORKDIR /aya-dev
# Copied this from CI, not sure if this is the right compilation command
RUN gradle jlinkAya --info --no-daemon --stacktrace --warning-mode all

FROM docker.io/library/debian:bookworm-slim
COPY --from=builder /aya-dev/ide-lsp/build/image/current /opt/aya
ENTRYPOINT ["/opt/aya/bin/aya"]

    The first part of the file is a separate stage for compilation. If Aya is compiled in advance, you can copy the generated JVM runtime from host instead, making the Containerfile only 3 lines long:

    FROM docker.io/library/debian:bookworm-slim
COPY ./ide-lsp/build/image/current /opt/aya
ENTRYPOINT ["/opt/aya/bin/aya"]

  2. Then you need to build and push to a registry, Docker Hub is the natural candidate. You'll need to create an account there. I suspect you'll want to build and push images via CI (I have no experience with Github Actions myself), but just for completeness, I've built and pushed example image like this:

    docker build . -t docker.io/wkarpiel/aya:latest
docker push docker.io/wkarpiel/aya:latest

    You can check it out:

    docker run --rm -it docker.io/wkarpiel/aya:latest --interactive

I'll gladly help with this, ask if you have any more questions!

  • ❤️1
ice1000 commented

I've built and pushed example image like this:

But does it work? If it works I can put this on the website

WojciechKarpiel commented

Yes, it works. The last command (docker run ...) will download the image (unless already present) and run the container, starting Aya REPL (--interactive Aya arg).
Feel free to use it, though keep in mind that this particular image is tied to my personal Docker Hub account. I've published the image as a proof of concept, I don't want to promise commitment to long term maintenance of the image.

  • ❤️1