search

domschrei / mallob

Malleable Load Balancer. Massively Parallel Logic Backend. Award-winning SAT solving for the cloud.
GNU Lesser General Public License v3.0
60 stars 16 forks source link

Building Docker fails to pull satcomp-base #14

Closed kenniskoldewyn closed 10 months ago

kenniskoldewyn commented 11 months ago

I'm trying to build mallob using Docker on Mac OS Sonoma 14.1.2 on a Macbook Pro with an M1 Max, and it fails immediately with the following error:

❯ cd docker/leader
❯ docker build -t mallob:leader ../.. -f ./Dockerfile
[+] Building 1.4s (3/3) FINISHED                                                                                                                                               docker:desktop-linux
 => [internal] load build definition from Dockerfile                                                                                                                                           0.0s
 => => transferring dockerfile: 3.75kB                                                                                                                                                         0.0s
 => [internal] load .dockerignore                                                                                                                                                              0.0s
 => => transferring context: 2B                                                                                                                                                                0.0s
 => ERROR [internal] load metadata for docker.io/library/satcomp-base:leader                                                                                                                   1.3s
------
 > [internal] load metadata for docker.io/library/satcomp-base:leader:
------
Dockerfile:47
--------------------
  45 |     
  46 |     ################### Extract Mallob in run stage
  47 | >>> FROM satcomp-base:leader AS mallob_liaison
  48 |     RUN whoami
  49 |     USER root
--------------------
ERROR: failed to solve: satcomp-base:leader: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed

Do you have any recommendations for pulling satcomp-base? I'm new to Docker, so maybe there's something obvious I'm missing.

domschrei commented 11 months ago

Hi, unfortunately the Dockerfiles are a bit outdated by now and the setup in there has been specialized to our distributed proof production in AWS. I'll try to drop an updated and self-contained Dockerfile some time.

What do you want to use Mallob for? If it's mainly for parallel/distributed SAT solving (without proof production), how about you use the Dockerfile from this year's SAT competition? See: https://github.com/domschrei/aws-batch-comp-infrastructure-sample/tree/mallob23

Your error specifically occurs because the Mallob image depends on a base image by the competition organizers. It's explained here (conveniently using my solver as an example): https://github.com/domschrei/aws-batch-comp-infrastructure-sample/blob/mallob23/docker/README-Solver-Development.md

kenniskoldewyn commented 11 months ago

Yes, I'd like to use Mallob for parallel/distributed SAT solving without proofs (and only on known satisfiable instances, so I'd be interested to know if Mallob can be optimized to save time by avoiding checks for unsatisfiability).

Using the Dockerfile from this year's SAT competition, I successfully built the SATComp base images but got a compilation error building the Mallob images (in YalSAT). Forcing the images to Intel rather than ARM via --platform linux/amd64 solved that problem, so I have successfully built Mallob. Thank you very much for your help!