[Bug 555161] Review Request: csisat - Tool for LA+EUF Interpolation

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=555161

--- Comment #6 from David A. Wheeler <dwheeler at dwheeler.com> 2010-01-19 16:09:29 EST ---
I can't rebuild this version.

I suspect that the parallelism isn't really working, and the resulting race
conditions cause build failures.  Doing this on an x86_64, Fedora 12.  When I
do "rpmbuild -ba csisat.spec", it fails; here are 3 attempts:

... TRY #1:
ocamlc.opt -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatAst.ml
mv  src/csisatUtils.o  obj/csisatUtils.o
mv  src/csisatAst.cmx obj/csisatAst.cmx
mv  src/csisatAst.cmi  obj/csisatAst.cmi
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/csisatAst.o  obj/csisatAst.o
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
40 states, 1373 transitions, table size 5732 bytes
ocamlopt.opt -inline 10 -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
obj/csisatInfixParse.ml
File "obj/csisatInfixParse.ml", line 1, characters 0-1:
Error: Could not find the .cmi file for interface obj/csisatInfixParse.mli.
make: *** [obj/csisatInfixParse.cmx] Error 2
error: Bad exit status from /var/tmp/rpm-tmp.IbC1EW (%build)



... TRY #2:
ocamlc.opt -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatUtils.ml
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
mv  src/csisatOrdSet.cmo  obj/csisatOrdSet.cmo
mv  src/csisatUtils.cmx obj/csisatUtils.cmx
mv  src/csisatUtils.cmi  obj/csisatUtils.cmi
mv  src/csisatOrdSet.o  obj/csisatOrdSet.o
mv  src/csisatUtils.cmo  obj/csisatUtils.cmo
mv  src/csisatUtils.o  obj/csisatUtils.o
ocamlopt.opt -inline 10 -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatAst.ml
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
ocamlopt.opt -inline 10 -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
obj/csisatInfixParse.ml
40 states, 1373 transitions, table size 5732 bytes
ocamlc.opt -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatAst.ml
File "src/io/csisatInfixParse.mly", line 20, characters 15-24:
Error: Unbound module CsisatAst
make: *** [obj/csisatInfixParse.cmx] Error 2
make: *** Waiting for unfinished jobs....
mv  src/csisatAst.cmx obj/csisatAst.cmx
mv  src/csisatAst.cmi  obj/csisatAst.cmi
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/csisatAst.o  obj/csisatAst.o
make: *** wait: No child processes.  Stop.
error: Bad exit status from /var/tmp/rpm-tmp.vZFA74 (%build)

RPM build errors:



... TRY #3:
ocamlc.opt -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatUtils.ml
mv  src/csisatUtils.cmx obj/csisatUtils.cmx
mv  src/csisatUtils.cmi  obj/csisatUtils.cmi
mv  src/csisatUtils.cmo  obj/csisatUtils.cmo
mv  src/csisatUtils.o  obj/csisatUtils.o
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamlc.opt -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
src/csisatAst.ml
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
40 states, 1373 transitions, table size 5732 bytes
ocamlopt.opt -inline 10 -I obj -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I
/home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c
obj/csisatInfixParse.ml
mv  src/csisatAst.cmx obj/csisatAst.cmx
File "src/io/csisatInfixParse.mly", line 20, characters 15-24:
Error: Unbound module CsisatAst
mv  src/csisatAst.cmi  obj/csisatAst.cmi
make: *** [obj/csisatInfixParse.cmx] Error 2
make: *** Waiting for unfinished jobs....
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/csisatAst.o  obj/csisatAst.o
error: Bad exit status from /var/tmp/rpm-tmp.C9VyuG (%build)


RPM build errors:
    Bad exit status from /var/tmp/rpm-tmp.C9VyuG (%build)

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.