diff --git a/cosmo-yices/Dockerfile b/cosmo-yices/Dockerfile index f47577e..d676034 100644 --- a/cosmo-yices/Dockerfile +++ b/cosmo-yices/Dockerfile @@ -60,6 +60,13 @@ RUN : \ COPY --from=downloader /gmp /gmp WORKDIR /gmp RUN : \ +# don't build this crap. our printf is fine. \ +# (i suppose this cause linking issues further down the \ +# line, but yices is fine without any of these symbols.) \ + && rm -r printf \ + && shed configure 's_ printf/Makefile _ _g' '/printf\/Makefile/d' \ + && shed Makefile.in 's_ printf _ _g' 's/$(PRINTF_OBJECTS) //g' \ +\ && CC=cosmocc CFLAGS="-O2 -g" \ # specify some generic old CPU for best compatibility/reproduciblity. \ # core2 introduced SSSE3, which cosmopolitan depends on, so use that: \ @@ -85,6 +92,10 @@ RUN : \ && shed src/utils/timeout.c '/#include /i\\#include ' \ # the static-lib target attempts to build a dynamic library. don't do that. \ && shed src/Makefile 's/ $(static_libyices_dynamic)//g' \ +# don't strip binaries; we'll do it ourselves later. \ + && shed src/Makefile '/^\t$(STRIP)/d' \ +# silence this irrelevant error. \ + && shed src/Makefile '/\*\.dll/d' \ \ && autoconf \ && CC=cosmocc \