search

domschrei / mallob

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

Building Docker #5

Open bratelefant opened 3 years ago

bratelefant commented 3 years ago

Hi dom,

again, congrats to your great results in 2021 sat race ;) I'm trying to build mallob on mac os for docker. I do docker build . in the root folder, and at first I get the following error:

...
 => CACHED [builder 8/9] RUN mkdir build                                   0.0s
 => CACHED [builder 9/9] RUN cd build && cmake -DCMAKE_BUILD_TYPE=RELEASE  0.0s
 => CACHED [mallob_liaison 2/8] COPY --from=builder build/mallob mallob    0.0s
 => CACHED [mallob_liaison 3/8] COPY --from=builder build/mallob_sat_proc  0.0s
 => CACHED [mallob_liaison 4/8] RUN chmod 755 mallob                       0.0s
 => CACHED [mallob_liaison 5/8] RUN chmod 755 mallob_sat_process           0.0s
 => CACHED [mallob_liaison 6/8] ADD mpi-run-aws.sh supervised-scripts/mpi  0.0s
 => CACHED [mallob_liaison 7/8] RUN chmod 755 supervised-scripts/mpi-run.  0.0s
 => ERROR [mallob_liaison 8/8] ADD test.cnf test.cnf                       0.0s
------
 > [mallob_liaison 8/8] ADD test.cnf test.cnf:
------
failed to compute cache key: "/test.cnf" not found: not found

After adding a random test.cnf file, the next reads

...
=> [builder 5/9] ADD CMakeLists.txt .                                     0.0s
 => [builder 6/9] RUN ls -lt                                               0.2s
 => ERROR [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh  0.8s
------                                                                          
 > [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh && cd ..:    
#15 0.311 Cloning into 'mergesat'...                                            
#15 0.721 Host key verification failed.                                         
#15 0.722 fatal: Could not read from remote repository.                         
#15 0.722                                                                       
#15 0.722 Please make sure you have the correct access rights                   
#15 0.722 and the repository exists.
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh && cd ..]: exit code: 128

Tried to workaround this by manually cloning mergesat and commenting out all git-related commands in fetch_and_build_sat_solvers.sh

But then the build fails while compiling minisat:

...
=> [builder 5/9] ADD CMakeLists.txt .                                     0.0s
 => [builder 6/9] RUN ls -lt                                               0.2s
 => ERROR [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh  5.7s
------                                                                          
 > [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh && cd ..:    
#15 0.159 sed: can't read mtl/*.cc: No such file or directory                   
#15 0.160 sed: can't read mtl/*.cc: No such file or directory                   
#15 0.161 sed: can't read mtl/*.cc: No such file or directory                   
#15 0.161 sed: can't read mtl/*.cc: No such file or directory                   
#15 0.225 Compiling: build/release/minisat/simp/Main.o                          
#15 0.226 Compiling: build/release/minisat/simp/ipasir.o
#15 0.226 Compiling: build/release/minisat/core/Solver.o
#15 0.226 Compiling: build/release/minisat/simp/SimpSolver.o
#15 0.499 minisat/simp/Main.cc: In function 'int main(int, char**)':
#15 0.499 minisat/simp/Main.cc:127:27: error: '_FPU_EXTENDED' was not declared in this scope
#15 0.499   127 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 0.499       |                           ^~~~~~~~~~~~~
#15 0.502 minisat/simp/Main.cc:127:44: error: '_FPU_DOUBLE' was not declared in this scope
#15 0.502   127 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 0.502       |                                            ^~~~~~~~~~~
#15 0.592 At global scope:
#15 0.592 cc1plus: warning: unrecognized command line option '-Wno-unknown-warning-option'
#15 0.603 make: *** [Makefile:148: build/release/minisat/simp/Main.o] Error 1
#15 0.603 make: *** Waiting for unfinished jobs....
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh && cd ..]: exit code: 2

I'm really not sure, weather my workarounds are legal, maybe there is a proper way of getting docker build . to work?

domschrei commented 3 years ago

Hi there, thank you!

Could you try if it works now with the latest changes?

bratelefant commented 3 years ago

Thanks for the quick patch; test.cnf error and fetching mergesat now works fine, but I still have this error during minisat build:

#15 1.267 mergesat/.gitignore
#15 1.275 Compiling: build/release/minisat/simp/Main.o
#15 1.276 Compiling: build/release/minisat/core/Solver.o
#15 1.277 Compiling: build/release/minisat/simp/ipasir.o
#15 1.277 Compiling: build/release/minisat/simp/SimpSolver.o
#15 1.654 minisat/simp/Main.cc: In function 'int main(int, char**)':
#15 1.654 minisat/simp/Main.cc:121:27: error: '_FPU_EXTENDED' was not declared in this scope
#15 1.654   121 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 1.654       |                           ^~~~~~~~~~~~~
#15 1.658 minisat/simp/Main.cc:121:44: error: '_FPU_DOUBLE' was not declared in this scope
#15 1.658   121 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 1.658       |                                            ^~~~~~~~~~~
#15 1.740 minisat/core/Solver.cc: In member function 'Minisat::Var Minisat::Solver::newVar(bool, bool)':
#15 1.740 minisat/core/Solver.cc:915:13: warning: suggest explicit braces to avoid ambiguous 'else' [-Wdangling-else]
#15 1.740   915 |     else if (init_act == 2)
#15 1.740       |             ^
#15 1.772 At global scope:
#15 1.772 cc1plus: warning: unrecognized command line option '-Wno-unknown-warning-option'
#15 1.789 make: *** [Makefile:147: build/release/minisat/simp/Main.o] Error 1
#15 1.790 make: *** Waiting for unfinished jobs....
#15 6.301 At global scope:
#15 6.301 cc1plus: warning: unrecognized command line option '-Wno-unknown-warning-option'
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh && cd ..]: exit code: 2
domschrei commented 3 years ago

Can you retry? It looks to me like MergeSat might have been missing an include of fpu_control.h, so I added it to the patched code.

bratelefant commented 3 years ago

Thanks Dom, now its working fine on my intel Mac, I'll give it a shot on my M1 machine later, but i guess the issue has been resolved now.

bratelefant commented 3 years ago

Sorry to bother again, but somehow the fpu_control.h error now reappears while building the current master branch.

domschrei commented 3 years ago

I'm sorry, I've been on vacation. Is it the same exact error at the same place?

Note that yesterday I added an option to compile Mallob with or without Mergesat (MALLOB_USE_MERGESAT=1, default 0) in the collectiveassignments branch. You might want to check whether it works on that branch.

lsorber commented 1 year ago

Hi, running docker build . still fails on master with the following output:

[+] Building 3.3s (8/10)
 => [internal] load build definition from Dockerfile                          0.0s
 => => transferring dockerfile: 810B                                          0.0s
 => [internal] load .dockerignore                                             0.0s
 => => transferring context: 2B                                               0.0s
 => [internal] load metadata for docker.io/library/ubuntu:20.04               1.1s
 => [1/7] FROM docker.io/library/ubuntu:20.04@sha256:9c2004872a3a9fcec8cc757  0.0s
 => CACHED [2/7] RUN apt-get update     && DEBIAN_FRONTEND=noninteractive ap  0.0s
 => CACHED [3/7] RUN git clone https://github.com/domschrei/mallob            0.0s
 => CACHED [4/7] WORKDIR mallob                                               0.0s
 => ERROR [5/7] RUN cd lib && bash fetch_and_build_sat_solvers.sh kcly && cd  2.1s
------
 > [5/7] RUN cd lib && bash fetch_and_build_sat_solvers.sh kcly && cd ..:
#8 0.172 --2022-10-14 15:44:36--  http://fmv.jku.at/yalsat/yalsat-03v.zip
#8 0.172 Resolving fmv.jku.at (fmv.jku.at)... 140.78.3.19
#8 0.178 Connecting to fmv.jku.at (fmv.jku.at)|140.78.3.19|:80... connected.
#8 0.209 HTTP request sent, awaiting response... 200 OK
#8 0.242 Length: 33679 (33K) [application/zip]
#8 0.243 Saving to: 'yalsat-03v.zip'
#8 0.243
#8 0.243      0K .......... .......... .......... ..                   100%  522K=0.06s
#8 0.307
#8 0.307 2022-10-14 15:44:36 (522 KB/s) - 'yalsat-03v.zip' saved [33679/33679]
#8 0.307
#8 0.311 --2022-10-14 15:44:36--  https://dominikschreiber.de/share/lingeling-isc22.zip
#8 0.312 Resolving dominikschreiber.de (dominikschreiber.de)... 85.13.157.89
#8 0.317 Connecting to dominikschreiber.de (dominikschreiber.de)|85.13.157.89|:443... connected.
#8 0.387 HTTP request sent, awaiting response... 200 OK
#8 0.422 Length: 255447 (249K) [application/zip]
#8 0.422 Saving to: 'lingeling-isc22.zip'
#8 0.422
#8 0.422      0K .......... .......... .......... .......... .......... 20%  800K 0s
#8 0.485     50K .......... .......... .......... .......... .......... 40% 1.53M 0s
#8 0.516    100K .......... .......... .......... .......... .......... 60% 12.4M 0s
#8 0.520    150K .......... .......... .......... .......... .......... 80% 1.53M 0s
#8 0.552    200K .......... .......... .......... .......... ......... 100%  181K=0.4s
#8 0.826
#8 0.826 2022-10-14 15:44:37 (619 KB/s) - 'lingeling-isc22.zip' saved [255447/255447]
#8 0.826
#8 0.844 --2022-10-14 15:44:37--  https://dominikschreiber.de/share/cadical-isc22.zip
#8 0.846 Resolving dominikschreiber.de (dominikschreiber.de)... 85.13.157.89
#8 0.855 Connecting to dominikschreiber.de (dominikschreiber.de)|85.13.157.89|:443... connected.
#8 0.929 HTTP request sent, awaiting response... 200 OK
#8 0.966 Length: 760938 (743K) [application/zip]
#8 0.966 Saving to: 'cadical-isc22.zip'
#8 0.966
#8 0.966      0K .......... .......... .......... .......... ..........  6%  654K 1s
#8 1.044     50K .......... .......... .......... .......... .......... 13% 1.52M 1s
#8 1.074    100K .......... .......... .......... .......... .......... 20% 6.55M 0s
#8 1.082    150K .......... .......... .......... .......... .......... 26% 1.81M 0s
#8 1.109    200K .......... .......... .......... .......... .......... 33% 9.38M 0s
#8 1.114    250K .......... .......... .......... .......... .......... 40% 12.8M 0s
#8 1.119    300K .......... .......... .......... .......... .......... 47% 13.7M 0s
#8 1.122    350K .......... .......... .......... .......... .......... 53% 1.77M 0s
#8 1.149    400K .......... .......... .......... .......... .......... 60% 23.6M 0s
#8 1.151    450K .......... .......... .......... .......... .......... 67% 7.14M 0s
#8 1.158    500K .......... .......... .......... .......... .......... 74% 2.88M 0s
#8 1.175    550K .......... .......... .......... .......... .......... 80% 4.99M 0s
#8 1.185    600K .......... .......... .......... .......... .......... 87% 8.71M 0s
#8 1.190    650K .......... .......... .......... .......... .......... 94% 10.7M 0s
#8 1.195    700K .......... .......... .......... .......... ...       100% 10.6M=0.2s
#8 1.199
#8 1.199 2022-10-14 15:44:37 (3.11 MB/s) - 'cadical-isc22.zip' saved [760938/760938]
#8 1.199
#8 1.204 --2022-10-14 15:44:37--  https://github.com/domschrei/kissat/archive/refs/heads/master.zip
#8 1.205 Resolving github.com (github.com)... 140.82.121.3
#8 1.210 Connecting to github.com (github.com)|140.82.121.3|:443... connected.
#8 1.247 HTTP request sent, awaiting response... 302 Found
#8 1.443 Location: https://codeload.github.com/domschrei/kissat/zip/refs/heads/master [following]
#8 1.447 --2022-10-14 15:44:37--  https://codeload.github.com/domschrei/kissat/zip/refs/heads/master
#8 1.447 Resolving codeload.github.com (codeload.github.com)... 140.82.121.9
#8 1.502 Connecting to codeload.github.com (codeload.github.com)|140.82.121.9|:443... connected.
#8 1.543 HTTP request sent, awaiting response... 200 OK
#8 1.718 Length: unspecified [application/zip]
#8 1.724 Saving to: 'master.zip'
#8 1.724
#8 1.724      0K .......... .......... .......... .......... .......... 1.60M
#8 1.754     50K .......... .......... .......... .......... .......... 2.75M
#8 1.776    100K .......... .......... .......... .......... .......... 7.02M
#8 1.779    150K .......... .......... .......... .......... .......... 4.34M
#8 1.790    200K .......... .......... .......... .......... .......... 11.9M
#8 1.795    250K .......... .......... .......... .......... .......... 15.0M
#8 1.798    300K .......... .......... .......... .......... .......... 11.4M
#8 1.802    350K .......... .......... .......... .......... .......... 6.43M
#8 1.811    400K .......... .......... .......... .......... .......... 3.84M
#8 1.822    450K .......... .......... .......... .......... .......... 3.91M
#8 1.834    500K .......... .......... .......... .......... .......... 3.18M
#8 1.850    550K .......... .......... .......... .......... .......... 5.99M
#8 1.858    600K .......... .......... .......... ........              30.9M=0.1s
#8 1.860
#8 1.860 2022-10-14 15:44:38 (4.60 MB/s) - 'master.zip' saved [653661]
#8 1.860
#8 1.866 Building YalSAT ...
#8 1.867 Archive:  yalsat-03v.zip
#8 1.867    creating: yalsat-03v/
#8 1.868   inflating: yalsat-03v/yals.h
#8 1.868   inflating: yalsat-03v/yils.h
#8 1.868   inflating: yalsat-03v/yals.c
#8 1.869  extracting: yalsat-03v/VERSION
#8 1.869   inflating: yalsat-03v/makefile.in
#8 1.869   inflating: yalsat-03v/config.c
#8 1.869   inflating: yalsat-03v/main.c
#8 1.870   inflating: yalsat-03v/LICENSE
#8 1.870   inflating: yalsat-03v/configure.sh
#8 1.870   inflating: yalsat-03v/README
#8 1.870   inflating: yalsat-03v/mkconfig.sh
#8 1.870   inflating: yalsat-03v/FILES
#8 1.881 gcc -Wall -DNDEBUG -O3 -lm
#8 1.884 gcc -Wall -DNDEBUG -O3 -c main.c
#8 1.928 main.c: In function 'printval':
#8 1.928 main.c:253:24: warning: '__builtin___sprintf_chk' may write a terminating nul past the end of the destination [-Wformat-overflow=]
#8 1.928   253 |   sprintf (buffer, " %d", lit);
#8 1.928       |                        ^
#8 1.928 In file included from /usr/include/stdio.h:867,
#8 1.928                  from yals.h:10,
#8 1.928                  from main.c:5:
#8 1.928 /usr/include/aarch64-linux-gnu/bits/stdio2.h:36:10: note: '__builtin___sprintf_chk' output between 3 and 13 bytes into a destination of size 12
#8 1.928    36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
#8 1.928       |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
#8 1.928    37 |       __bos (__s), __fmt, __va_arg_pack ());
#8 1.928       |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
#8 1.999 gcc -Wall -DNDEBUG -O3 -c yals.c
#8 2.017 yals.c: In function 'yals_set_fpu':
#8 2.017 yals.c:499:15: error: '_FPU_EXTENDED' undeclared (first use in this function)
#8 2.017   499 |   control &= ~_FPU_EXTENDED;
#8 2.017       |               ^~~~~~~~~~~~~
#8 2.017 yals.c:499:15: note: each undeclared identifier is reported only once for each function it appears in
#8 2.018 yals.c:500:15: error: '_FPU_SINGLE' undeclared (first use in this function)
#8 2.018   500 |   control &= ~_FPU_SINGLE;
#8 2.018       |               ^~~~~~~~~~~
#8 2.019 yals.c:501:14: error: '_FPU_DOUBLE' undeclared (first use in this function)
#8 2.019   501 |   control |= _FPU_DOUBLE;
#8 2.019       |              ^~~~~~~~~~~
#8 2.048 make: *** [makefile:18: yals.o] Error 1
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh kcly && cd ..]: exit code: 2

Looks like fpu_control.h is missing in yalsat.

domschrei commented 1 year ago

Hi there, sorry for the late reply, we're working on a paper with a tight deadline right now.

The problem with fpu_control.h is occurring whenever building on architectures which don't support the FPU magic done in YalSAT. Could you add this line:

sed -i 's/#ifdef __linux__/#if 0/g' yals.c

between line 51 and line 52 of lib/fetch_and_build_sat_solvers.sh and report what happens? With this line I've fixed this problem before on different branches. I know that CryptoMinisat has an automatic process for turning this on and off, but I didn't have the time to integrate something like this so far.