#!/usr/bin/false if [ ! -e /cosmo-yices.done ]; then : \ && acquire from=github repo=SRI-CSL/yices2 dest=/root/yices env=YICES \ \ && remote_fn="gmp-$GMP_VERSION.tar.xz" \ && export local_fn="$remote_fn" \ && export remote_url="https://gmplib.org/download/gmp/$remote_fn" \ && export dest=/root/gmp \ && export sha256="$GMP_SHA256" \ && acquire \ \ && acquire from=github repo=arminbiere/kissat dest=/root/kissat env=KISSAT \ \ && cd /root/kissat \ && shed src/application.c '/#include /i\\#include ' \ && shed configure '/passtocompiler -fpic/i\\CFLAGS=" -O2 -g -Wall"' \ && CC=cosmocc ./configure \ && make -j2 \ && install -m 0644 -D -t /usr/local/lib build/libkissat.a \ && install -m 0644 -D -t /usr/local/include -m644 src/kissat.h \ \ && cd /root/gmp \ && 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" \ ac_cv_build='core2-pc-linux-gnu' \ ac_cv_host='core2-pc-linux-gnu' \ gmp_cv_c_double_format='IEEE little endian' \ quickconf --disable-shared \ && make -j2 \ && make install \ \ && cd /root/yices \ && shed src/context/context.c 's/\bdonothing\b/&_/g' \ && shed src/terms/bv_constants.c 's/\bhextoint\b/&_/g' \ && shed src/terms/bv64_constants.c 's/\bhextoint\b/&_/g' \ && shed src/utils/timeout.c '/#include /i\\#include ' \ && shed src/Makefile 's/ $(static_libyices_dynamic)//g' \ && shed src/Makefile '/^\t$(STRIP)/d' \ && shed src/Makefile '/\*\.dll/d' \ && autoconf \ && CC=cosmocc \ CFLAGS="-O2 -g" \ CPPFLAGS="-I/usr/local/include -DHAVE_KISSAT" \ LDFLAGS="-L/usr/local/lib" \ LIBS="-lkissat" \ quickconf --prefix= \ && make -j2 static-dist \ && mv build/x86_64-pc-linux-gnu-release/static_dist dist \ && cd dist/bin \ && for bin in yices yices-sat yices-smt yices-smt2 \ ;do : \ && mv "$bin" "$bin.com.dbg" \ && objcopy -S -O binary "$bin.com.dbg" "$bin.com" \ ;done \ && cd /root/kissat/build \ && mv "kissat" "kissat.com.dbg" \ && objcopy -S -O binary "kissat.com.dbg" "kissat.com" \ \ && touch /cosmo-yices.done \ || exit $? fi