search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
478 stars 72 forks source link

How to build the multiplataform docker image on macos? #137

Closed brando90 closed 4 months ago

brando90 commented 4 months ago

Description I tried building the docker image on a mac with multiplataform but if failed.

Detailed Steps to Reproduce the Behavior Command I ran:

docker buildx build --platform linux/amd64,linux/arm64 -t brandojazz/lean-dojo:latest --push .

Logs in Debug Mode

❯ docker buildx build --platform linux/amd64,linux/arm64 -t brandojazz/lean-dojo:latest --push .
[+] Building 0.0s (0/0)                                                                                                                     docker:desktop-linux
ERROR: Multi-platform build is not supported for the docker driver.
Switch to a different driver, or turn on the containerd image store, and try again.
Learn more at https://docs.docker.com/go/build-multi-platform/

Platform Information

cross: https://stackoverflow.com/questions/78054282/how-to-build-the-multiplataform-docker-image-on-macos ref: https://docs.docker.com/build/building/multi-platform/ ref: https://chat.openai.com/c/69a268e3-122e-4a61-9577-4dc5ef693922

brando90 commented 4 months ago

for now this worked

If buildx doesn't work then create the docker image for your plataform:
```bash
cd $HOME/gold-ai-olympiad/docker

# Build the Image
docker build -t brandojazz/lean-dojo:latest .

# Push the Image to a Docker Registry
docker push brandojazz/lean-dojo:latest

# Start the Docker Container, -d, it runs the container in the background 
docker run -d --name lean-dojo-container brandojazz/lean-dojo:latest
# docker run -it --name lean-dojo-container brandojazz/lean-dojo:latest bash

# Attach to the running Docker container via a terminal CLI bash
docker exec -it lean-dojo-container bash

I think...failed actually

brando90 commented 4 months ago

related, what would be a good base image instead of https://hub.docker.com/r/kitware/cmake/tags?page=1

FROM kitware/cmake:ci-clang_cxx_modules-x86_64-2023-02-15

perhaps that solves the issue fixing the dockerfile

# Use a specific version of kitware/cmake as the base image
FROM kitware/cmake:ci-clang_cxx_modules-x86_64-2023-02-15

# Install required packages: 'which', GMP library development files, Python3, and pip
RUN yum -y install which gmp-devel python3 python3-pip
# Create a symbolic link for python3 as /usr/bin/python for compatibility
RUN ln -s $(which python3) /usr/bin/python
# Install Python packages: toml for TOML file parsing, loguru for logging, tqdm for progress bars
RUN pip3 install toml loguru tqdm

# Set the environment variable ELAN_HOME to store Elan's installation
ENV ELAN_HOME="/.elan"
# Add ELAN_HOME/bin to the PATH for easier access to Elan's binaries
ENV PATH="${ELAN_HOME}/bin:${PATH}"
# Download and execute Elan's installation script in silent mode with auto-approval
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y

# Change permissions to allow writing in the /.elan directory
RUN chmod -R a+w /.elan

# Set the working directory to /workspace for the container
WORKDIR /workspace
# Change permissions to allow writing in the /workspace directory
RUN chmod -R a+w /workspace
yangky11 commented 4 months ago

Hi @brando90,

I remember I had similar issues but didn't find a good solution, due to complexities in Docker's multi-platform builds.

I'm wondering if Docker is really needed in your use case. The most recent version of LeanDojo is designed to work smoothly without Docker. Unless you're working with Lean 3, you might not need Docker.