diff --git a/notwa-util/cosmo-yices11 b/notwa-util/cosmo-yices11 new file mode 100755 index 0000000..0a12149 --- /dev/null +++ b/notwa-util/cosmo-yices11 @@ -0,0 +1,67 @@ +#!/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 \ + && unset local_fn remote_url dest sha256 \ +\ + && 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' \ + ./configure --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" \ + ./configure --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" \ + && x86_64-linux-musl-objcopy -S -O binary "$bin.com.dbg" "$bin.com" \ + && zipcopy.com "$bin.com.dbg" "$bin.com" \ + ;done \ + && cd /root/kissat/build \ + && mv "kissat" "kissat.com.dbg" \ + && x86_64-linux-musl-objcopy -S -O binary "kissat.com.dbg" "kissat.com" \ + && zipcopy.com "kissat.com.dbg" "kissat.com" \ +\ + && touch /cosmo-yices.done \ + || exit $? +fi diff --git a/notwa-util/doit11 b/notwa-util/doit11 index b1ef851..4cfd384 100755 --- a/notwa-util/doit11 +++ b/notwa-util/doit11 @@ -37,7 +37,8 @@ YICES_SHA256=d4aa3bedbc143516f8db57f189f96e09a1771f31215c16b4c13bcdca38f592e3 \ if [ ! -e /notwa-util.done ]; then : \ && cd /vagrant/notwa-util \ - && install -p -m 0755 -t /usr/local/bin/ acquire dedupe expand makeit ofc quickconf shed \ + && install -p -m 0755 -t /usr/local/bin/ \ + acquire dedupe expand makeit ofc quickconf shed \ && touch /notwa-util.done \ || exit $? fi @@ -59,6 +60,7 @@ sed \ -e 's,/libc/crt/,/dist/$MODE/,g' \ -e 's,/o/$MODE/,/,g' \ -e 's,/ape/,/dist/$MODE/,g' \ +-e "s,\$MODE\\b,$MODE,g" \ -i /usr/bin/cosmocc cd /root && export PATH="$COSMO/bin:$COSMO/gcc/bin:$PATH" || exit $? @@ -66,9 +68,8 @@ unset V COLUMNS TMPDIR . /vagrant/notwa-util/cosmo-kuroko11 || exit $? # . /vagrant/notwa-util/cosmo-mini11 || exit $? # . /vagrant/notwa-util/cosmo-muon11 || exit $? -unset CC CFLAGS -# . /vagrant/notwa-util/cosmo-yices11 || exit $? -unset local_fn remote_url dest sha256 +unset CC CFLAGS MODE mode +. /vagrant/notwa-util/cosmo-yices11 || exit $? : \ && cd /root \ @@ -85,10 +86,10 @@ unset local_fn remote_url dest sha256 `#muon/build/muon.com` \ `#selfie/selfie.com` \ `#xe/xe.com` \ - `#yices/dist/bin/yices-sat.com` \ - `#yices/dist/bin/yices-smt.com` \ - `#yices/dist/bin/yices-smt2.com` \ - `#yices/dist/bin/yices.com` \ + yices/dist/bin/yices-sat.com \ + yices/dist/bin/yices-smt.com \ + yices/dist/bin/yices-smt2.com \ + yices/dist/bin/yices.com \ ;do : \ && du -k "$com" \ && install -p -m 0755 -t /vagrant/out/vagrant "$com" \