Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

YICES_STUB option leads to build failure #599

Open
Vekhir opened this issue Aug 13, 2023 · 3 comments
Open

YICES_STUB option leads to build failure #599

Vekhir opened this issue Aug 13, 2023 · 3 comments

Comments

@Vekhir
Copy link
Contributor

Vekhir commented Aug 13, 2023 •
edited
Loading

Issue

When using the build option YICES_STUB=1 during building in order to disable Yices, BSC fails to build with error

/build/bluespec-git/src/bsc/inst/bin/bsc -stdlib-names -bdir /build/bluespec-git/src/bsc/build/bsvlib -p . -vsearch /build/bluespec-git/src/bsc/build/bsvlib -no-use-prelude Prelude.bs
Error: Command line: (S0081)
  The flag `-sat-yices' was used, but a proper shared object file was not
  found. Please specify a different SAT solver or check that the
  LD_LIBRARY_PATH or BLUESPEC_LD_LIBRARY_PATH includes a valid `libyices.so.2'
  file.

Apparently, building with Yices disabled still requires Yices to build? If I had to guess, then probably the logic to choose the default solver fails to switch to STP if Yices isn't available.
The buiild fails when the standard library is being compiled.

Additional information

Error occurs on the main branch (commit 0b38555). Omitting the build option builds just fine. The exact same issue happens on commit 0352270 from Nov 2020, which is the oldest one I can test with my GHC compiler.

Command: make YICES_STUB=1 GHC="ghc -dynamic" GHCJOBS=4 GHCRTSFLAGS='+RTS -M5G -A128m -RTS' install-src

Command (0352270): make YICES_STUB=1 GHC="ghc -dynamic" GHCJOBS=4 GHCRTSFLAGS='+RTS -M5G -A128m -RTS' install

System information

OS: Arch Linux
Kernel: 6.4.9-arch1-1
GHC: 9.0.2-3
BSC: 0b38555 and 0352270 (via bluespec-git)

Full error log 
make  -C src  PREFIX=/build/bluespec-git/src/bsc/inst  install
make[1]: Entering directory '/build/bluespec-git/src/bsc/src'
make  -C vendor/stp   PREFIX=/build/bluespec-git/src/bsc/inst  install
make[2]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp'
make -C src install
make[3]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp/src'
make -C AST 
make -C sat core
make[4]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/AST'
make[4]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat'
make LIB="core" -C core libr
Making dependencies
make[5]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core'
Making dependencies
Compiling: /build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.or
Compiling: utils/Options.or
Compiling: utils/System.or
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/System.od'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/System.op'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/System.o'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/Options.od'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/Options.op'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '../utils/Options.o'.
./genkinds.pl
Making dependencies
../mtl/template.mk:71: warning: pattern recipe did not update peer target '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.od'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.op'.
../mtl/template.mk:71: warning: pattern recipe did not update peer target '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.o'.
Making library: libcore_release.a ( /build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.or utils/Options.or utils/System.or )
a - /build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core/Solver.or
a - ../utils/Options.or
a - ../utils/System.or
Making Soft Link: libcore_release.a -> libcore.a
make[5]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core'
make LIB="core_prop" -C core_prop libr
make[5]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat/core_prop'
Making dependencies

[Building STP...]

make[4]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/stp/src/sat'
mkdir -p lib
rm -f lib/libstp.so.1
g++ -march=x86-64 -mtune=generic -O2 -pipe -fno-plt -fexceptions         -Wp,-D_FORTIFY_SOURCE=2 -Wformat -Werror=format-security         -fstack-clash-protection -fcf-protection -O3 -DNDEBUG -fomit-frame-pointer -fPIC  -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -shared  -Wl,-soname,libstp.so.1 -o lib/libstp.so.1 -Lto-sat -Wl,--whole-archive -ltosat -Wl,--no-whole-archive c_interface/c_interface.o extlib-constbv/libconstantbv.a extlib-abc/libabc.a STPManager/libstpmgr.a simplifier/libsimplifier.a absrefine_counterexample/libabstractionrefinement.a AST/libast.a printer/libprinter.a sat/libminisat.a cpp_interface/libcppinterface.a parser/libparser.a main/libmain.a
rm -f lib/libstp.so
(cd lib; ln -s libstp.so.1 libstp.so)
mkdir -p ../lib
mkdir -p ../include
cp -df lib/libstp.so.1 lib/libstp.so ../lib
cp -df c_interface/*.h ../include
mv ../include/c_interface.h ../include/stp_c_interface.h
make[3]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/stp/src'
ln -fsn HaskellIfc include_hs
install -m 755 -d /build/bluespec-git/src/bsc/inst/lib/SAT
install -m 644 lib/libstp.so.1 /build/bluespec-git/src/bsc/inst/lib/SAT
make[2]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/stp'
make  -C vendor/yices PREFIX=/build/bluespec-git/src/bsc/inst  install
make[2]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/yices'
make -C v2.6 install
make[3]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/yices/v2.6'
(cd stub ; make install)
make[4]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/yices/v2.6/stub'
cc -c -Wall -fPIC  -I../yices2/src/include -o yices.o yices.c
cc -shared -Wl,-soname,libyices.so.2.6 -o libyices.so.2.6.stub yices.o
ln -sf libyices.so.2.6.stub libyices.so.2.6
ln -sf libyices.so.2.6.stub libyices.so
mkdir -p ../yices2-inst/lib
cp -df libyices.so.2.6.stub libyices.so.2.6 libyices.so  ../yices2-inst/lib/
mkdir -p ../yices2-inst/include
cp -df ../yices2/src/include/yices.h ../yices2/src/include/yices_types.h ../yices2/src/include/yices_limits.h  ../yices2-inst/include/
make[4]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/yices/v2.6/stub'
ln -fsn /build/bluespec-git/src/bsc/src/vendor/yices/v2.6/yices2-inst/include
ln -fsn /build/bluespec-git/src/bsc/src/vendor/yices/v2.6/yices2-inst/lib
ln -fsn HaskellIfc include_hs
make[3]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/yices/v2.6'
ln -fsn v2.6/include
ln -fsn v2.6/lib
ln -fsn v2.6/include_hs
install -m 755 -d /build/bluespec-git/src/bsc/inst/lib/SAT
install -m 644 lib/libyices.so.2.6 /build/bluespec-git/src/bsc/inst/lib/SAT
make[2]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/yices'
make  -C vendor/htcl  PREFIX=/build/bluespec-git/src/bsc/inst  install
make[2]: Entering directory '/build/bluespec-git/src/bsc/src/vendor/htcl'
Using tclsh: /usr/bin/tclsh
Using tcl include flags: 
Using tcl library flags: -ltcl8.6 -ltclstub8.6
ghc -dynamic -Wall  -c haskell.c
ar -r libhtcl.a haskell.o
ar: creating libhtcl.a
make[2]: Leaving directory '/build/bluespec-git/src/bsc/src/vendor/htcl'
# we need to build targets from here sequentially, as they operate in the same workspace
make  -C comp -j1   PREFIX=/build/bluespec-git/src/bsc/inst  install
make[2]: Entering directory '/build/bluespec-git/src/bsc/src/comp'
make[2]: warning: -j1 forced in submake: resetting jobserver mode.
Using tclsh: /usr/bin/tclsh
Using tcl include flags: 
Using tcl library flags: -ltcl8.6 -ltclstub8.6
Building with GHC 9.0.2
----- Normal build options -----
./update-build-version.sh
./update-build-system.sh
bsc start Sun Aug 13 23:23:08 CEST 2023
./update-build-version.sh
BuildVersion.hs up-to-date
./update-build-system.sh
BuildSystem.hs up-to-date
ghc -dynamic -hidir /build/bluespec-git/src/bsc/src/comp/../../build/comp -odir /build/bluespec-git/src/bsc/src/comp/../../build/comp -stubdir /build/bluespec-git/src/bsc/src/comp/../../build/comp -main-is Main_bsc \
	-O2 -hide-all-packages -fasm -Wall -fno-warn-orphans -fno-warn-name-shadowing -fno-warn-unused-matches -package base -package containers -package array -package mtl -package unix -package regex-compat -package bytestring -package directory -package process -package filepath -package time -package old-time -package old-locale -package split -package syb -package integer-gmp  -iGHC -iGHC/posix -iLibs -i../Parsec -i../vendor/stp/include_hs -i../vendor/yices/include_hs -i../vendor/htcl '-tmpdir /tmp'  -I../vendor/stp/include -I../vendor/yices/include -L../vendor/htcl   -lpthread --make bsc -j4 +RTS -M5G -A128m -RTS "-with-rtsopts=-H256m -K10m -i1" -rtsopts -L../vendor/stp/lib -lstp -L../vendor/yices/lib -lyices 
[  1 of 226] Compiling BDD              ( BDD.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BDD.o )
[  2 of 226] Compiling Bag              ( Bag.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Bag.o )
[  3 of 226] Compiling BinaryIO         ( GHC/BinaryIO.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BinaryIO.o )
[  4 of 226] Compiling BuildSystem      ( BuildSystem.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BuildSystem.o )
[  5 of 226] Compiling BuildVersion     ( BuildVersion.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BuildVersion.o )
[  6 of 226] Compiling EquivalenceClass ( EquivalenceClass.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/EquivalenceClass.o )
[  7 of 226] Compiling Exceptions       ( Exceptions.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Exceptions.o )
[  8 of 226] Compiling Fixity           ( Fixity.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Fixity.o )
[  9 of 226] Compiling GraphPaths       ( GraphPaths.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GraphPaths.o )
[ 10 of 226] Compiling IOMutVar         ( Libs/IOMutVar.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IOMutVar.o )
[ 11 of 226] Compiling Classic          ( Classic.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Classic.o )
[ 12 of 226] Compiling IOUtil           ( Libs/IOUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IOUtil.o )
[ 13 of 226] Compiling ListMap          ( Libs/ListMap.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ListMap.o )
[ 14 of 226] Compiling ListUtil         ( Libs/ListUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ListUtil.o )
[ 15 of 226] Compiling Log2             ( Log2.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Log2.o )
[ 16 of 226] Compiling Parse            ( Libs/Parse.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parse.o )
[ 17 of 226] Compiling RealUtil         ( RealUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/RealUtil.o )
[ 18 of 226] Compiling SEMonad          ( SEMonad.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SEMonad.o )
[ 19 of 226] Compiling STPFFI           ( ../vendor/stp/include_hs/STPFFI.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/STPFFI.o )
[ 20 of 226] Compiling Sort             ( Libs/Sort.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Sort.o )
[ 21 of 226] Compiling SystemVerilogKeywords ( SystemVerilogKeywords.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemVerilogKeywords.o )
[ 22 of 226] Compiling TmpNam           ( GHC/posix/TmpNam.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TmpNam.o )
[ 23 of 226] Compiling Version          ( Version.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Version.o )
[ 24 of 226] Compiling ErrorUtil        ( ErrorUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ErrorUtil.o )
[ 25 of 226] Compiling Util             ( Util.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Util.o )
[ 26 of 226] Compiling FileNameUtil     ( FileNameUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/FileNameUtil.o )
[ 27 of 226] Compiling SpeedyString     ( SpeedyString.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SpeedyString.o )
[ 28 of 226] Compiling IntegerUtil      ( IntegerUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IntegerUtil.o )
[ 29 of 226] Compiling GHCPretty        ( GHCPretty.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GHCPretty.o )
[ 30 of 226] Compiling Pretty           ( Pretty.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Pretty.o )
[ 31 of 226] Compiling PPrint           ( PPrint.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PPrint.o )
[ 32 of 226] Compiling PVPrint          ( PVPrint.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PVPrint.o )
[ 33 of 226] Compiling Intervals        ( Intervals.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Intervals.o )
[ 34 of 226] Compiling GraphMap         ( GraphMap.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GraphMap.o )
[ 35 of 226] Compiling FStringCompat    ( FStringCompat.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/FStringCompat.o )
[ 36 of 226] Compiling PreStrings       ( PreStrings.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PreStrings.o )
[ 37 of 226] Compiling Eval             ( Eval.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Eval.o )
[ 38 of 226] Compiling VFileName        ( VFileName.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VFileName.o )
[ 39 of 226] Compiling Undefined        ( Undefined.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Undefined.o )
[ 40 of 226] Compiling Position         ( Position.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Position.o )
[ 41 of 226] Compiling MVarStrict       ( Libs/MVarStrict.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/MVarStrict.o )
[ 42 of 226] Compiling STP              ( ../vendor/stp/include_hs/STP.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/STP.o )
[ 43 of 226] Compiling IntLit           ( IntLit.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IntLit.o )
[ 44 of 226] Compiling Literal          ( Literal.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Literal.o )
[ 45 of 226] Compiling Id               ( Id.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Id.o )
[ 46 of 226] Compiling Verilog          ( Verilog.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Verilog.o )
[ 47 of 226] Compiling VPrims           ( VPrims.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VPrims.o )
[ 48 of 226] Compiling VVerilogDollar   ( VVerilogDollar.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VVerilogDollar.o )
[ 49 of 226] Compiling PreIds           ( PreIds.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PreIds.o )
[ 50 of 226] Compiling NumType          ( NumType.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/NumType.o )
[ 51 of 226] Compiling GraphWrapper     ( GraphWrapper.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GraphWrapper.o )
[ 52 of 226] Compiling GraphUtil        ( GraphUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GraphUtil.o )
[ 53 of 226] Compiling ConTagInfo       ( ConTagInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ConTagInfo.o )
[ 54 of 226] Compiling BoolExp          ( BoolExp.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BoolExp.o )
[ 55 of 226] Compiling Backend          ( Backend.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Backend.o )
[ 56 of 226] Compiling Flags            ( Flags.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Flags.o )
[ 57 of 226] Compiling PFPrint          ( PFPrint.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PFPrint.o )
[ 58 of 226] Compiling SchedInfo        ( SchedInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SchedInfo.o )
[ 59 of 226] Compiling Error            ( Error.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Error.o )
[ 60 of 226] Compiling SystemVerilogTokens ( SystemVerilogTokens.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemVerilogTokens.o )
[ 61 of 226] Compiling SystemVerilogScanner ( SystemVerilogScanner.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemVerilogScanner.o )
[ 62 of 226] Compiling SystemCheck      ( SystemCheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemCheck.o )
[ 63 of 226] Compiling ProofObligation  ( ProofObligation.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ProofObligation.o )
[ 64 of 226] Compiling Prim             ( Prim.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Prim.o )
[ 65 of 226] Compiling ParsecPrim       ( ../Parsec/ParsecPrim.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ParsecPrim.o )
[ 66 of 226] Compiling ParsecCombinator ( ../Parsec/ParsecCombinator.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ParsecCombinator.o )
[ 67 of 226] Compiling ParsecExpr       ( ../Parsec/ParsecExpr.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ParsecExpr.o )
[ 68 of 226] Compiling ParsecChar       ( ../Parsec/ParsecChar.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ParsecChar.o )
[ 69 of 226] Compiling Parsec           ( ../Parsec/Parsec.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parsec.o )
[ 70 of 226] Compiling Lex              ( Lex.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Lex.o )
[ 71 of 226] Compiling IdPrint          ( IdPrint.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IdPrint.o )
[ 72 of 226] Compiling VModInfo         ( VModInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VModInfo.o )
[ 73 of 226] Compiling Pragma           ( Pragma.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Pragma.o )
[ 74 of 226] Compiling FlagsDecode      ( FlagsDecode.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/FlagsDecode.o )
[ 75 of 226] Compiling FileIOUtil       ( FileIOUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/FileIOUtil.o )
[ 76 of 226] Compiling ErrorMonad       ( ErrorMonad.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ErrorMonad.o )
[ 77 of 226] Compiling DOT              ( DOT.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/DOT.o )
[ 78 of 226] Compiling CType            ( CType.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CType.o )
[ 79 of 226] Compiling Type             ( Type.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Type.o )
[ 80 of 226] Compiling Subst            ( Subst.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Subst.o )
[ 81 of 226] Compiling Unify            ( Unify.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Unify.o )
[ 82 of 226] Compiling PragmaCheck      ( PragmaCheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PragmaCheck.o )
[ 83 of 226] Compiling CSyntax          ( CSyntax.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CSyntax.o )
[ 84 of 226] Compiling PoisonUtils      ( PoisonUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/PoisonUtils.o )
[ 85 of 226] Compiling ParseOp          ( ParseOp.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ParseOp.o )
[ 86 of 226] Compiling GenWrapUtils     ( GenWrapUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenWrapUtils.o )
[ 87 of 226] Compiling CSyntaxUtil      ( CSyntaxUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CSyntaxUtil.o )
[ 88 of 226] Compiling IConvLet         ( IConvLet.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IConvLet.o )
[ 89 of 226] Compiling CVPrint          ( CVPrint.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CVPrint.o )
[ 90 of 226] Compiling KIMisc           ( KIMisc.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/KIMisc.o )
[ 91 of 226] Compiling CSyntaxTypes     ( CSyntaxTypes.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CSyntaxTypes.o )
[ 92 of 226] Compiling Pred             ( Pred.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Pred.o )
[ 93 of 226] Compiling Scheme           ( Scheme.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Scheme.o )
[ 94 of 226] Compiling Assump           ( Assump.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Assump.o )
[ 95 of 226] Compiling SymTab           ( SymTab.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SymTab.o )
[ 96 of 226] Compiling TIMonad          ( TIMonad.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TIMonad.o )
[ 97 of 226] Compiling StdPrel          ( StdPrel.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/StdPrel.o )
[ 98 of 226] Compiling IType            ( IType.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IType.o )
[ 99 of 226] Compiling IStateLoc        ( IStateLoc.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IStateLoc.o )
[100 of 226] Compiling Pred2STP         ( Pred2STP.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Pred2STP.o )
[101 of 226] Compiling CPPLineDirectives ( CPPLineDirectives.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CPPLineDirectives.o )
[102 of 226] Compiling SystemVerilogPreprocess ( SystemVerilogPreprocess.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemVerilogPreprocess.o )
[103 of 226] Compiling CFreeVars        ( CFreeVars.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CFreeVars.o )
[104 of 226] Compiling Parser.Classic.Warnings ( Parser/Classic/Warnings.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/Classic/Warnings.o )
[105 of 226] Compiling Parser.BSV.CVParserCommon ( Parser/BSV/CVParserCommon.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV/CVParserCommon.o )
[106 of 226] Compiling Parser.BSV.CVParserUtil ( Parser/BSV/CVParserUtil.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV/CVParserUtil.o )
[107 of 226] Compiling Parser.BSV.CVParserAssertion ( Parser/BSV/CVParserAssertion.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV/CVParserAssertion.o )
[108 of 226] Compiling Parser.BSV.CVParserImperative ( Parser/BSV/CVParserImperative.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV/CVParserImperative.o )
[109 of 226] Compiling InferKind        ( InferKind.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/InferKind.o )
[110 of 226] Compiling CSubst           ( CSubst.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CSubst.o )
[111 of 226] Compiling CCSyntax         ( CCSyntax.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CCSyntax.o )
[112 of 226] Compiling BoolOpt          ( BoolOpt.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BoolOpt.o )
[113 of 226] Compiling BinParse         ( BinParse.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BinParse.o )
[114 of 226] Compiling Parser.Classic.CParser ( Parser/Classic/CParser.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/Classic/CParser.o )
[115 of 226] Compiling Parser.Classic   ( Parser/Classic.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/Classic.o )
[116 of 226] Compiling Balanced         ( Balanced.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Balanced.o )
[117 of 226] Compiling SCC              ( SCC.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SCC.o )
[118 of 226] Compiling Simplify         ( Simplify.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Simplify.o )
[119 of 226] Compiling MakeSymTab       ( MakeSymTab.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/MakeSymTab.o )
[120 of 226] Compiling Wires            ( Wires.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Wires.o )
[121 of 226] Compiling ISyntax          ( ISyntax.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISyntax.o )
[122 of 226] Compiling InstNodes        ( InstNodes.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/InstNodes.o )
[123 of 226] Compiling IWireSet         ( IWireSet.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IWireSet.o )
[124 of 226] Compiling ISyntaxXRef      ( ISyntaxXRef.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISyntaxXRef.o )
[125 of 226] Compiling ISyntaxUtil      ( ISyntaxUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISyntaxUtil.o )
[126 of 226] Compiling ISimplify        ( ISimplify.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISimplify.o )
[127 of 226] Compiling IPrims           ( IPrims.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IPrims.o )
[128 of 226] Compiling IInlineUtil      ( IInlineUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IInlineUtil.o )
[129 of 226] Compiling IInline          ( IInline.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IInline.o )
[130 of 226] Compiling IDropRules       ( IDropRules.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IDropRules.o )
[131 of 226] Compiling FixupDefs        ( FixupDefs.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/FixupDefs.o )
[132 of 226] Compiling BExpr            ( BExpr.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BExpr.o )
[133 of 226] Compiling ITransform       ( ITransform.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ITransform.o )
[134 of 226] Compiling ISplitIf         ( ISplitIf.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISplitIf.o )
[135 of 226] Compiling ILift            ( ILift.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ILift.o )
[136 of 226] Compiling ASyntax          ( ASyntax.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ASyntax.o )
[137 of 226] Compiling TopUtils         ( TopUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TopUtils.o )
[138 of 226] Compiling Parser.BSV.CVParser ( Parser/BSV/CVParser.lhs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV/CVParser.o )
[139 of 226] Compiling Parser.BSV       ( Parser/BSV.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Parser/BSV.o )
[140 of 226] Compiling SimDomainInfo    ( SimDomainInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimDomainInfo.o )
[141 of 226] Compiling SignalNaming     ( SignalNaming.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SignalNaming.o )
[142 of 226] Compiling Params           ( Params.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Params.o )
[143 of 226] Compiling BinData          ( BinData.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BinData.o )
[144 of 226] Compiling GenBin           ( GenBin.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenBin.o )
[145 of 226] Compiling BinUtil          ( BinUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BinUtil.o )
[146 of 226] Compiling BackendNamingConventions ( BackendNamingConventions.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BackendNamingConventions.o )
[147 of 226] Compiling ASyntaxUtil      ( ASyntaxUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ASyntaxUtil.o )
[148 of 226] Compiling VIOProps         ( VIOProps.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VIOProps.o )
[149 of 226] Compiling VFinalCleanup    ( VFinalCleanup.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VFinalCleanup.o )
[150 of 226] Compiling SimPrimitiveModules ( SimPrimitiveModules.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimPrimitiveModules.o )
[151 of 226] Compiling InlineWires      ( InlineWires.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/InlineWires.o )
[152 of 226] Compiling InlineCReg       ( InlineCReg.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/InlineCReg.o )
[153 of 226] Compiling ForeignFunctions ( ForeignFunctions.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ForeignFunctions.o )
[154 of 226] Compiling SimCCBlock       ( SimCCBlock.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimCCBlock.o )
[155 of 226] Compiling IInlineFmt       ( IInlineFmt.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IInlineFmt.o )
[156 of 226] Compiling DPIWrappers      ( DPIWrappers.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/DPIWrappers.o )
[157 of 226] Compiling AVerilogUtil     ( AVerilogUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AVerilogUtil.o )
[158 of 226] Compiling VPIWrappers      ( VPIWrappers.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/VPIWrappers.o )
[159 of 226] Compiling InlineReg        ( InlineReg.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/InlineReg.o )
[160 of 226] Compiling AVerilog         ( AVerilog.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AVerilog.o )
[161 of 226] Compiling AVeriQuirks      ( AVeriQuirks.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AVeriQuirks.o )
[162 of 226] Compiling AUses            ( AUses.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AUses.o )
[163 of 226] Compiling RSchedule        ( RSchedule.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/RSchedule.o )
[164 of 226] Compiling ATaskSplice      ( ATaskSplice.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ATaskSplice.o )
[165 of 226] Compiling AScheduleInfo    ( AScheduleInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AScheduleInfo.o )
[166 of 226] Compiling ARenameIO        ( ARenameIO.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ARenameIO.o )
[167 of 226] Compiling ARemoveAssumps   ( ARemoveAssumps.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ARemoveAssumps.o )
[168 of 226] Compiling ARankMethCalls   ( ARankMethCalls.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ARankMethCalls.o )
[169 of 226] Compiling APaths           ( APaths.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/APaths.o )
[170 of 226] Compiling ANoInline        ( ANoInline.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ANoInline.o )
[171 of 226] Compiling AExpr2Util       ( AExpr2Util.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AExpr2Util.o )
[172 of 226] Compiling AExpr2STP        ( AExpr2STP.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AExpr2STP.o )
[173 of 226] Compiling ADumpScheduleInfo ( ADumpScheduleInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ADumpScheduleInfo.o )
[174 of 226] Compiling ADropUndet       ( ADropUndet.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ADropUndet.o )
[175 of 226] Compiling AConv            ( AConv.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AConv.o )
[176 of 226] Compiling AExpand          ( AExpand.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AExpand.o )
[177 of 226] Compiling ADropDefs        ( ADropDefs.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ADropDefs.o )
[178 of 226] Compiling ACheck           ( ACheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ACheck.o )
[179 of 226] Compiling ABin             ( ABin.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ABin.o )
[180 of 226] Compiling GenABin          ( GenABin.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenABin.o )
[181 of 226] Compiling GenForeign       ( GenForeign.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenForeign.o )
[182 of 226] Compiling ABinUtil         ( ABinUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ABinUtil.o )
[183 of 226] Compiling SimPackage       ( SimPackage.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimPackage.o )
[184 of 226] Compiling SystemCWrapper   ( SystemCWrapper.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SystemCWrapper.o )
[185 of 226] Compiling SimFileUtils     ( SimFileUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimFileUtils.o )
[186 of 226] Compiling SimBlocksToC     ( SimBlocksToC.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimBlocksToC.o )
[187 of 226] Compiling SimMakeCBlocks   ( SimMakeCBlocks.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimMakeCBlocks.o )
[188 of 226] Compiling SimExpand        ( SimExpand.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimExpand.o )
[189 of 226] Compiling SimCOpt          ( SimCOpt.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimCOpt.o )
[190 of 226] Compiling AAddScheduleDefs ( AAddScheduleDefs.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AAddScheduleDefs.o )
[191 of 226] Compiling YicesFFI         ( ../vendor/yices/include_hs/YicesFFI.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/YicesFFI.o )
[192 of 226] Compiling Yices            ( ../vendor/yices/include_hs/Yices.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Yices.o )
[193 of 226] Compiling Pred2Yices       ( Pred2Yices.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Pred2Yices.o )
[194 of 226] Compiling SATPred          ( SATPred.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SATPred.o )
[195 of 226] Compiling TCMisc           ( TCMisc.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TCMisc.o )
[196 of 226] Compiling TCPat            ( TCPat.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TCPat.o )
[197 of 226] Compiling ISyntaxCheck     ( ISyntaxCheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ISyntaxCheck.o )
[198 of 226] Compiling IExpandUtils     ( IExpandUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IExpandUtils.o )
[199 of 226] Compiling IConv            ( IConv.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IConv.o )
[200 of 226] Compiling IfcBetterInfo    ( IfcBetterInfo.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IfcBetterInfo.o )
[201 of 226] Compiling Deriving         ( Deriving.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Deriving.o )
[202 of 226] Compiling CtxRed           ( CtxRed.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/CtxRed.o )
[203 of 226] Compiling ContextErrors    ( ContextErrors.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ContextErrors.o )
[204 of 226] Compiling TCheck           ( TCheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TCheck.o )
[205 of 226] Compiling TypeCheck        ( TypeCheck.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TypeCheck.o )
[206 of 226] Compiling IExpand          ( IExpand.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/IExpand.o )

IExpand.hs:3671:13: warning:
    Pattern match checker ran into -fmax-pmcheck-models=30 limit, so
      • Redundant clauses might not be reported at all
      • Redundant clauses might be reported as inaccessible
      • Patterns reported as unmatched might actually be matched
    Increase the limit or resolve the warnings to suppress this message.
     |
3671 |             case doPrimOp bestPosition op
     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

IExpand.hs:3671:13: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative:
        Patterns not matched:
            Just _
            Just _
            Just _
            Just _
            ...
     |
3671 |             case doPrimOp bestPosition op
     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
[207 of 226] Compiling GenWrap          ( GenWrap.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenWrap.o )
[208 of 226] Compiling GenSign          ( GenSign.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenSign.o )
[209 of 226] Compiling GenFuncWrap      ( GenFuncWrap.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GenFuncWrap.o )
[210 of 226] Compiling Depend           ( Depend.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Depend.o )
[211 of 226] Compiling AExpr2Yices      ( AExpr2Yices.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AExpr2Yices.o )
[212 of 226] Compiling SAT              ( SAT.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SAT.o )
[213 of 226] Compiling AProofs          ( AProofs.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AProofs.o )
[214 of 226] Compiling AOpt             ( AOpt.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AOpt.o )
[215 of 226] Compiling Synthesize       ( Synthesize.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Synthesize.o )
[216 of 226] Compiling SimPackageOpt    ( SimPackageOpt.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SimPackageOpt.o )
[217 of 226] Compiling LambdaCalcUtil   ( LambdaCalcUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/LambdaCalcUtil.o )
[218 of 226] Compiling SAL              ( SAL.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/SAL.o )
[219 of 226] Compiling LambdaCalc       ( LambdaCalc.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/LambdaCalc.o )
[220 of 226] Compiling ADumpSchedule    ( ADumpSchedule.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ADumpSchedule.o )
[221 of 226] Compiling DisjointTest     ( DisjointTest.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/DisjointTest.o )
[222 of 226] Compiling ASchedule        ( ASchedule.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ASchedule.o )
[223 of 226] Compiling AState           ( AState.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AState.o )
[224 of 226] Compiling AAddSchedAssumps ( AAddSchedAssumps.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/AAddSchedAssumps.o )
[225 of 226] Compiling ACleanup         ( ACleanup.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/ACleanup.o )
[226 of 226] Compiling Main_bsc         ( bsc.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/Main_bsc.o )
Linking bsc ...
bsc done Sun Aug 13 23:26:21 CEST 2023

bluetcl start Sun Aug 13 23:26:22 CEST 2023
ghc -dynamic -hidir /build/bluespec-git/src/bsc/src/comp/../../build/comp -odir /build/bluespec-git/src/bsc/src/comp/../../build/comp -stubdir /build/bluespec-git/src/bsc/src/comp/../../build/comp -O2 -hide-all-packages -fasm -Wall -fno-warn-orphans -fno-warn-name-shadowing -fno-warn-unused-matches -package base -package containers -package array -package mtl -package unix -package regex-compat -package bytestring -package directory -package process -package filepath -package time -package old-time -package old-locale -package split -package syb -package integer-gmp  -iGHC -iGHC/posix -iLibs -i../Parsec -i../vendor/stp/include_hs -i../vendor/yices/include_hs -i../vendor/htcl '-tmpdir /tmp'  -I../vendor/stp/include -I../vendor/yices/include -L../vendor/htcl   -lpthread --make bluetcl -j4 +RTS -M5G -A128m -RTS -c
[144 of 150] Compiling GlobPattern      ( GlobPattern.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/GlobPattern.o )
[145 of 150] Compiling HTcl             ( ../vendor/htcl/HTcl.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/HTcl.o )
[146 of 150] Compiling TclUtils         ( TclUtils.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TclUtils.o )
[147 of 150] Compiling BluesimLoader    ( BluesimLoader.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BluesimLoader.o )
[148 of 150] Compiling TypeAnalysis     ( TypeAnalysis.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TypeAnalysis.o )
[149 of 150] Compiling TypeAnalysisTclUtil ( TypeAnalysisTclUtil.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/TypeAnalysisTclUtil.o )
[150 of 150] Compiling BlueTcl          ( bluetcl.hs, /build/bluespec-git/src/bsc/src/comp/../../build/comp/BlueTcl.o )
ghc -dynamic -hidir /build/bluespec-git/src/bsc/src/comp/../../build/comp -odir /build/bluespec-git/src/bsc/src/comp/../../build/comp -stubdir /build/bluespec-git/src/bsc/src/comp/../../build/comp -O2 -hide-all-packages -fasm -Wall -fno-warn-orphans -fno-warn-name-shadowing -fno-warn-unused-matches -package base -package containers -package array -package mtl -package unix -package regex-compat -package bytestring -package directory -package process -package filepath -package time -package old-time -package old-locale -package split -package syb -package integer-gmp  -iGHC -iGHC/posix -iLibs -i../Parsec -i../vendor/stp/include_hs -i../vendor/yices/include_hs -i../vendor/htcl '-tmpdir /tmp'  -I../vendor/stp/include -I../vendor/yices/include -L../vendor/htcl   -lpthread --make bluetcl -j4 +RTS -M5G -A128m -RTS -L../vendor/stp/lib -lstp -L../vendor/yices/lib -lyices  -ltcl8.6 -ltclstub8.6 -lhtcl  \
	-o bluetcl \
	-no-hs-main \
	-x c bluetcl_Main.hsc
Linking bluetcl ...
bluetcl done Sun Aug 13 23:26:41 CEST 2023

mkdir -p -m 755 /build/bluespec-git/src/bsc/inst/bin/core
install -m 755 bsc /build/bluespec-git/src/bsc/inst/bin/core/bsc
mkdir -p -m 755 /build/bluespec-git/src/bsc/inst/bin
install -m 755 wrapper.sh /build/bluespec-git/src/bsc/inst/bin/bsc
mkdir -p -m 755 /build/bluespec-git/src/bsc/inst/bin/core
install -m 755 bluetcl /build/bluespec-git/src/bsc/inst/bin/core/bluetcl
mkdir -p -m 755 /build/bluespec-git/src/bsc/inst/bin
install -m 755 wrapper.sh /build/bluespec-git/src/bsc/inst/bin/bluetcl
make[2]: Leaving directory '/build/bluespec-git/src/bsc/src/comp'
make  -C Libraries  PREFIX=/build/bluespec-git/src/bsc/inst  install
make[2]: Entering directory '/build/bluespec-git/src/bsc/src/Libraries'
make -C Base1 build &&  make -C Base2 build &&  make -C Base3-Misc build &&  make -C Base3-Contexts build &&  make -C Base3-Math build && true
make[3]: Entering directory '/build/bluespec-git/src/bsc/src/Libraries/Base1'
mkdir -p /build/bluespec-git/src/bsc/build/bsvlib
/build/bluespec-git/src/bsc/inst/bin/bsc -stdlib-names -bdir /build/bluespec-git/src/bsc/build/bsvlib -p . -vsearch /build/bluespec-git/src/bsc/build/bsvlib -no-use-prelude Prelude.bs
Error: Command line: (S0081)
  The flag `-sat-yices' was used, but a proper shared object file was not
  found. Please specify a different SAT solver or check that the
  LD_LIBRARY_PATH or BLUESPEC_LD_LIBRARY_PATH includes a valid `libyices.so.2'
  file.
make[3]: *** [Makefile:26: /build/bluespec-git/src/bsc/build/bsvlib/Prelude.bo] Error 1
make[3]: Leaving directory '/build/bluespec-git/src/bsc/src/Libraries/Base1'
make[2]: *** [Makefile:31: build] Error 2
make[2]: Leaving directory '/build/bluespec-git/src/bsc/src/Libraries'
make[1]: *** [Makefile:62: install] Error 2
make[1]: Leaving directory '/build/bluespec-git/src/bsc/src'
make: *** [GNUmakefile:41: install-src] Error 2
@Vekhir
Copy link
Contributor Author

Vekhir commented Aug 13, 2023

And for similar reasons as #595, the option won't work on macOS at all, because no .dylib is created, only .so.

@quark17
Copy link
Collaborator

quark17 commented Aug 14, 2023

There is no logic to choose the default (it's always Yices) and there is no fall-back if it's not available -- see the message for commit 49760f3. That means that a build with Yices stub would need to have -sat-stp explicitly provided every time. That does seem unfriendly.

The check for the solver (and error if it's a stub) is done in checkSATFlags in SAT.hs. We could change that function to try other solvers if a stub is found. We could change the type of satBackend in Flags to be a Maybe that starts as Nothing, so that it captures whether a solver was specifically requested. In theory, the build of bsc could consult the makefile flags and hardcode STP as the default, if Yices is built as a stub; but I'm not sure I want to go that route.

@Vekhir
Copy link
Contributor Author

Vekhir commented Aug 14, 2023

I'm not sure we are on the same page.

The issue isn't so much that I'd have to pass -sat-stp everywhere to use BSC, rather, I cannot use it at all because the flag isn't passed during the build process of this very library itself.

So using YICES_STUB means that there is no package at all, because the build fails.

@Vekhir Vekhir mentioned this issue Aug 14, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@quark17 @Vekhir