From af94fd544f439b9ab57a21648ca6b045da3e3a51 Mon Sep 17 00:00:00 2001
From: colepoirier <colepoirier@gmail.com>
Date: Mon, 18 May 2020 12:55:13 -0700
Subject: [PATCH] Significantly simplfied yosys and related tools installation
 script

---
 yosys-et-al | 137 ++++++++++++++++++++++++++++------------------------
 1 file changed, 73 insertions(+), 64 deletions(-)

diff --git a/yosys-et-al b/yosys-et-al
index 1e73470..e214c59 100755
--- a/yosys-et-al
+++ b/yosys-et-al
@@ -1,81 +1,90 @@
-mkdir hdl
-cd hdl
+#!/bin/bash
+if [ "$EUID" -ne 0 ]
+  then echo "Please run as root"
+  exit
+fi
+
+export MYNAME=`id 1000 | awk '{print $1}' | sed 's/.*(\(.*\))/\1/'`
+export MYHOME=/home/$MYNAME
+
+runuser $MYNAME --preserve-environment -c '
+cd /home/$MYNAME
+mkdir hdl_tools
+cd hdl_tools
+
 git clone https://github.com/cliffordwolf/yosys.git
-cd yosys
+git clone https://github.com/YosysHQ/SymbiYosys.git sby
+git clone https://github.com/SRI-CSL/yices2.git
+git clone https://github.com/Z3Prover/z3.git
+'
+cd /home/$MYNAME/hdl_tools/yosys
 make config-clang
 make -j$(nproc)
-make -j$(nproc) test
 make install
 
-cd ../
-git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys
-cd SymbiYosys
+cd ../sby
 make install
 
-cd ../
-git clone https://github.com/SRI-CSL/yices2.git yices2
-cd yices2
+cd ../yices2
 autoconf
 ./configure
 make -j$(nproc)
 make install
 
-cd ../
-git clone https://github.com/Z3Prover/z3.git z3
-cd z3
+cd ../z3
 python scripts/mk_make.py
 cd build
 make -j$(nproc)
 make install
 
-cd ../../
-hg clone https://bitbucket.org/sterin/super_prove_build
-cd super_prove_build
-patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
---- a/MetaSat/MiniSat2/System.cc	Thu Sep 14 01:44:08 2017 -0700
-+++ b/MetaSat/MiniSat2/System.cc	Thu May 14 20:10:24 2020 +0000
-@@ -20,6 +20,7 @@
- 
- #include <signal.h>
- #include <stdio.h>
-+#include <stdlib.h>
- 
- #include "System.hh"
- 
-@@ -27,7 +28,6 @@
- 
- #if defined(__linux__)
- 
--#include <stdlib.h>
- 
- static inline int memReadStat(int field)
- {
-")
-patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
---- a/Bip/Main_bip.cc	Thu Sep 14 01:44:08 2017 -0700
-+++ b/Bip/Main_bip.cc	Thu May 14 20:08:52 2020 +0000
-@@ -508,8 +508,8 @@
- void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
- {
-     Vec<Pair<int,GLit> > ffs, pis;
--    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
--    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
-+    For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w));
-+    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI  (w).number, w));
-     sort(ffs);
-     sort(pis);                             
- 
-")
-mkdir build && cd build
-cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
-ninja
-ninja package
-SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
-tar xvf $SPBIN -C /usr/local/bin/
-cat << "EOF" > /usr/local/bin/suprove
-#!/bin/bash
-tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
-exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
-EOF
-chmod +x /usr/local/bin/suprove
-suprove
+#cd ../../
+#hg clone https://bitbucket.org/sterin/super_prove_build
+#cd super_prove_build
+#patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
+#--- a/MetaSat/MiniSat2/System.cc	Thu Sep 14 01:44:08 2017 -0700
+#+++ b/MetaSat/MiniSat2/System.cc	Thu May 14 20:10:24 2020 +0000
+#@@ -20,6 +20,7 @@
+# 
+# #include <signal.h>
+# #include <stdio.h>
+#+#include <stdlib.h>
+# 
+# #include "System.hh"
+# 
+#@@ -27,7 +28,6 @@
+# 
+# #if defined(__linux__)
+# 
+#-#include <stdlib.h>
+# 
+# static inline int memReadStat(int field)
+# {
+#")
+#patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
+#--- a/Bip/Main_bip.cc	Thu Sep 14 01:44:08 2017 -0700
+#+++ b/Bip/Main_bip.cc	Thu May 14 20:08:52 2020 +0000
+#@@ -508,8 +508,8 @@
+# void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
+# {
+#     Vec<Pair<int,GLit> > ffs, pis;
+#-    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
+#-    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
+#+    For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w));
+#+    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI  (w).number, w));
+#     sort(ffs);
+#     sort(pis);                             
+# 
+#")
+#mkdir build && cd build
+#cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
+#ninja
+#ninja package
+#SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
+#tar xvf $SPBIN -C /usr/local/bin/
+#cat << "EOF" > /usr/local/bin/suprove
+##!/bin/bash
+#tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
+#exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
+#EOF
+#chmod +x /usr/local/bin/suprove
+#suprove
-- 
2.30.2