yices2
yices2 copied to clipboard
SRI-CSL
Question about distributions.
So I make a distribution for 2.6.3 and I see:
>tree .
.
├── LICENSE
├── NOTICES
├── README
├── bin
│ ├── yices
│ ├── yices-sat
│ ├── yices-smt
│ └── yices-smt2
├── doc
│ ├── YICES-LANGUAGE
│ └── manual.pdf
├── etc
│ └── pstdint.h
├── examples
│ ├── abs_axiom.smt2
.
.
.
│ ├── tst_bvult1.smt
│ └── tst_bvult2.smt
├── include
│ ├── yices.h
│ ├── yices_exit_codes.h
│ ├── yices_limits.h
│ └── yices_types.h
├── install-yices
└── lib
├── libyices.a
└── libyices.so.2.6.4
6 directories, 195 files
But if I do:
> ldd bin/yices-smt2
linux-vdso.so.1 (0x00007fffc25f5000)
libcudd-3.0.0.so.0 => /usr/local/lib/libcudd-3.0.0.so.0 (0x00007fe000e5e000)
libpoly.so.0 => /usr/local/lib/libpoly.so.0 (0x00007fe000e0e000)
libgmp.so.10 => /lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fe000d8a000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fe000c3b000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fe000a49000)
libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fe000867000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fe00084a000)
/lib64/ld-linux-x86-64.so.2 (0x00007fe000f14000)
or
>ldd lib/libyices.so.2.6.4
linux-vdso.so.1 (0x00007fff1fba9000)
libcudd-3.0.0.so.0 => /usr/local/lib/libcudd-3.0.0.so.0 (0x00007f2c217cc000)
libpoly.so.0 => /usr/local/lib/libpoly.so.0 (0x00007f2c2177c000)
libgmp.so.10 => /lib/x86_64-linux-gnu/libgmp.so.10 (0x00007f2c216f8000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f2c215a9000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f2c213b7000)
libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f2c211d5000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f2c211b8000)
/lib64/ld-linux-x86-64.so.2 (0x00007f2c21a7f000)
I see that we depend on libpoly and cudd, but don't include them in the distro. Is this right? Does this mean that to make an offline install I should make my own tar ball?
OK so the static distribution is almost what I want, but not quite:
ldd lib/libyices.so.2.6.4
linux-vdso.so.1 (0x00007ffe11a83000)
libcudd-3.0.0.so.0 => /usr/local/lib/libcudd-3.0.0.so.0 (0x00007f24a54bb000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f24a536c000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f24a517a000)
libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f24a4f98000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f24a4f7d000)
/lib64/ld-linux-x86-64.so.2 (0x00007f24a57f7000)
The build still depends on the cudd dynamic library. This is a bug right @BrunoDutertre?
Yes
ls -la /usr/local/lib/libcudd.a
-rw-r--r-- 1 vagrant vagrant 6093152 Oct 2 18:09 /usr/local/lib/libcudd.a
and it is PIC too.
readelf --relocs /usr/local/lib/libcudd.a | awk '$3~/^R_/ && $5!~/^\.debug/{print $3}' |sort -u
R_X86_64_64
R_X86_64_GOTPCREL
R_X86_64_PC32
R_X86_64_PLT32
Let me run through the build again, and see if I screwed up somewhere along the way...
I don't think you screwed up anything. The problem is that you have two versions of libcudd. That doesn't happen to me. I only get 'libcudd.a' (but I always build cudd from source).
A quick fix is to edit configs/make.include.x86_64-pc-linux-gnu and replace '-lcudd' in
there by '/usr/local/lib/libcudd.a'.
I am building CUDD from source too, so do I just configure it with --disable-shared?
I would prefer a non hacky solution because I will be doing it repeatedly for a while I think.
I am also building libpoly from source, and it doesn't install the pic lib that it builds ¯\_(ツ)_/¯
Interesting. I thought --disable-shared was the default for cudd.
When I run ./configure in cudd (without any flags), it prints this:
--------------------------------------------------
Configuration summary for cudd 3.0.0
Build system : x86_64-unknown-linux-gnu
Host system : x86_64-unknown-linux-gnu
Prefix : '/usr/local'
Compilers : 'gcc -Wall -Wextra -fPIC -g -O3'
: 'g++ -Wall -Wextra -fPIC -std=c++0x -g -O3'
Shared library : no
dddmp enabled : no
obj enabled : no
--------------------------------------------------
Yes I guess it was the default (I did some cut and paste from my homebrew Formulii).
TLDR;
ldd libyices.so.2.6.4
linux-vdso.so.1 (0x00007ffebc257000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f58b7889000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f58b7697000)
/lib64/ld-linux-x86-64.so.2 (0x00007f58b7cc9000)
Happy happy joy joy
One last question. What version of GMP do you think we should use to please the "customer" and include in the binaries of the release when we get there? The current stable release is 6.2.1, released 2020-11-14.
The tricky part is to get a pic version of libgmp.a. If you already have one, I wouldn't upgrade to a new version of GMP. Otherwise, the latest GMP should be fine.
Same problem with the darwin build, but I moved the dynamic versions of libcudd out of the way and that fixed it. Poor libcudd, all the other dependencies get a --with-static-whatever configure flag, but not libcudd.
For the darwin build I had to resort to editing configs/make.include.x86_64-apple-darwin18.7.0 and replace -lpoly with ...libpoly-0.1.11-x86_64-apple-darwin/lib/libpoly.a because it kept using a non-existant /usr/local/opt/libpoly.dylib.
Gotta find that cache and trash it.
So let see if I can concisely describe the two times I got bit by the -lpoly in building a
distro where the shared libyices contains the code from libpoly and libcudd.
On Linux I am using libpicpoly.a but the configure script looks for lp_polynomial_new via -lpoly
so I have to fool it by renaming libpicpoly.a to libpoly.a
On Darwin I couldn't convince it that /usr/local/opt/libpoly.dylib didn't exist, and had to eventually resort to editing configs/make.include.x86_64-apple-darwin18.7.0 and replace -lpoly with .../libpoly.a because it kept using a non-existent /usr/local/opt/libpoly.dylib. Maybe finding that
cache and changing its mind could work here.