Container image for Aya

[WojciechKarpiel]

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]

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

[ice1000]

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]

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!

[ice1000]

I've built and pushed example image like this:

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

[WojciechKarpiel]

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.