1:BUILD_BY[name] student0 1:BUILD_ENVIRONMENT[operating system 32 vs 64] 1:END_BUILD_ENVIRONMENT 1:DEPENDENCIES[list of dependencies with where to get them] - gcc and ocaml need to be installed on the system - Yices SMT solver, which we are not allowed to redistribute due to licensing restrictions. The tools are known to work with version 1.0.28/1.0.29 with dynamically linked GMP which you can obtain from http://yices.csl.sri.com/ You can then use the script deps/ocamlyices/install-yices.sh to install yices. - camlidl. Version 1.05 is bundled with this distribution, you can install it as follows: cd deps/camlidl-1.05 make sudo make install - curses library is required by CIL 1:END_DEPENDENCIES 1:NOTES[notes on attempted build] make returned an error. [ 13%] Generating src/symtrace/imltrace, src/symtrace/pitrace, src/symtrace/cvtrace /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.so when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.a when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.so when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.a when searching for -lyices /usr/bin/ld: cannot find -lyices collect2: ld returned 1 exit status File "caml_startup", line 1, characters 0-1: Error: Error during linking make[3]: *** [imltrace] Error 2 make[2]: *** [src/symtrace/imltrace] Error 2 make[1]: *** [CMakeFiles/CSur.dir/all] Error 2 make: *** [all] Error 2 1:END_NOTES 2:BUILD_BY[name] student3 2:BUILD_ENVIRONMENT[operating system 32 vs 64] Ubuntu 13.10 x64 2:END_BUILD_ENVIRONMENT 2:DEPENDENCIES[list of dependencies with where to get them] - gcc and ocaml need to be installed on the system - Yices SMT solver, which we are not allowed to redistribute due to licensing restrictions. The tools are known to work with version 1.0.28/1.0.29 with dynamically linked GMP which you can obtain from http://yices.csl.sri.com/ You can then use the script deps/ocamlyices/install-yices.sh to install yices. - camlidl. Version 1.05 is bundled with this distribution, you can install it as follows: cd deps/camlidl-1.05 make sudo make install - curses library is required by CIL 2:END_DEPENDENCIES 2:NOTES[notes on attempted build] After getting gmp, yices, autoconf, and camlidl on my machine it is still giving this error: student@student:~/repro/ccs12/AizatulinGJ12/src/csec-modex$ make [ 0%] Generating deps/ocamlyices/ocamlyices.cmxa, deps/ocamlyices/yices.cmi running CONFIG_SHELL=/bin/bash /bin/bash ./configure --enable-custom --no-create --no-recursion checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking for ranlib... ranlib checking for ocamlc... ocamlc configure: ocaml version is 4.01.0 configure: ocaml library path is /home/student/.opam/4.01.0/lib/ocaml checking for ocamlfind... ocamlfind checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamldoc... ocamldoc checking for camlidl... camlidl checking platform... *nix checking for __gmpz_init... no configure: GMP needed: try to detect best version checking for Yices' shared library... /usr/local/lib/libyices.so.2.2 /usr/local/lib/libyices.so checking GMP dependency of Yices' shared library... unknown, fallback to default checking for __gmpq_init... yes configure: creating ./config.status config.status: creating Makefile In file included from yices_stubs.c:17:0: yices.h:18:21: fatal error: yices_c.h: No such file or directory #include ^ compilation terminated. make[3]: *** [yices_stubs.o] Error 1 make[2]: *** [deps/ocamlyices/ocamlyices.cmxa] Error 2 make[1]: *** [CMakeFiles/CSur.dir/all] Error 2 make: *** [all] Error 2 ~Note: I figured out I was using yice 2, instead of the required (but no longer supported) yice 1.0.28. When I installed that, using their script(deps/ocamlyices/install-yices.sh) and run make again I get this error: student@student:~/repro/ccs12/AizatulinGJ12/src/csec-modex$ make [ 0%] Generating src/symtrace/imltrace, src/symtrace/pitrace, src/symtrace/cvtrace File "execute.ml", line 117, characters 10-20: Warning 26: unused variable checkOrder. /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.so when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.a when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.so when searching for -lyices /usr/bin/ld: skipping incompatible /usr/local/lib/libyices.a when searching for -lyices /usr/bin/ld: cannot find -lyices collect2: error: ld returned 1 exit status File "caml_startup", line 1: Error: Error during linking make[3]: *** [imltrace] Error 2 make[2]: *** [src/symtrace/imltrace] Error 2 make[1]: *** [CMakeFiles/CSur.dir/all] Error 2 make: *** [all] Error 2 ~Note: I had to to a link from ln /usr/local/lib/libgmp.so.10 /usr/local/lib/libgmp.so.3 else there would be an error where it could not find a compatiable version of GMP, but with this link it builds and checks without a problem. 2:END_NOTES