get yices building again

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 <unistd.h>/i\\#include <time.h>' \
+ && 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 <unistd.h>/i\\#include <time.h>' \
+ && 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

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" \