This is the base image which is intended to be used by evaluation functions written in Lean 4. It is based on the debian:bookworm-slim image and adds the necessary components to run evaluation functions written in Lean 4.
This image is not meant to be run directly. Instead, it ought to be used as a base image for evaluation functions written in Lean 4. The evaluation function should be placed in the /app directory.
Here is an example of a Dockerfile that uses this image as a base:
FROM ghcr.io/lambda-feedback/evaluation-function-base/lean:latest as build
COPY . .
RUN lake build
FROM ghcr.io/lambda-feedback/evaluation-function-base/scratch:latest
COPY --from=build /app/.lake/build/bin/evaluation_function /app/evaluation_function
ENV FUNCTION_COMMAND="/app/evaluation_function"