Opened 13 years ago
Last modified 6 years ago
#32627 assigned defect
nusmv: universal variant fails
Reported by: | ryandesign (Ryan Carsten Schmidt) | Owned by: | |
---|---|---|---|
Priority: | Normal | Milestone: | |
Component: | ports | Version: | 2.0.3 |
Keywords: | universal | Cc: | cooljeanius (Eric Gallager) |
Port: | nusmv |
Description
main.log says:
:info:configure checking for MiniSat_Create in -lMiniSat... no :info:configure configure: error: MiniSat library not found in /opt/local/var/macports/build/_Users_rschmidt_macports_dports_devel_nusmv/nusmv/work/NuSMV-2.5.4/MiniSat/minisat
config.log says:
configure:21259: checking for MiniSat_Create in -lMiniSat configure:21295: ccache /usr/bin/gcc-4.2 -std=gnu99 -o conftest -fno-strict-aliasing -pipe -O2 -arch x86_64 -arch i386 -I/opt/local/include -L/opt/local/lib -arch x86_64 -arch i386 conftest.c -lMiniSat -L/opt/local/var/macports/build/_Users_rschmidt_macports_dports_devel_nusmv/nusmv/work/NuSMV-2.5.4/MiniSat/minisat -lstdc++ -lm >&5 ld: warning: in /opt/local/var/macports/build/_Users_rschmidt_macports_dports_devel_nusmv/nusmv/work/NuSMV-2.5.4/MiniSat/minisat/libMiniSat.a, file was built for unsupported file format which is not the architecture being linked (i386) Undefined symbols for architecture i386: "_MiniSat_Create", referenced from: _main in ccKlyUhX.o ld: symbol(s) not found for architecture i386 collect2: ld returned 1 exit status lipo: can't open input file: /var/tmp//ccjlyCnC.out (No such file or directory) configure:21302: $? = 1
This can be fixed by replacing ${configure.cc_archflags}
with [get_canonical_archflags cc]
and ${configure.cxx_archflags}
with [get_canonical_archflags cxx]
, but that's not the whole story, and I don't believe that results in correct software.
I'm also concerned about these lines from main.log:
:info:configure checking size of void *... 8 :info:configure checking size of int... 4 :info:configure checking size of long... 8 :info:configure checking size of long long... 8
Those values would not necessarily be accurate for all of the architectures being built.
I'm also concerned about these lines from the Portfile:
if {$build_arch == "x86_64"} { system -W ${worksrcpath}/cudd-2.4.1.1 "mv Makefile_os_x_64bit Makefile_os_x" }
Shouldn't this take effect for ppc64 as well, not just for x86_64?
And what about universal builds? The difference between the two Makefiles is:
-XCFLAGS = -DHAVE_IEEE_754 -DBSD -D__MAC_OS_X__ -DNUSMV_SIZEOF_VOID_P=4 -DNUSMV_SIZEOF_LONG=4 -DNUSMV_SIZEOF_INT=4 +XCFLAGS = -DHAVE_IEEE_754 -DBSD -D__MAC_OS_X__ -DNUSMV_SIZEOF_VOID_P=8 -DNUSMV_SIZEOF_LONG=8 -DNUSMV_SIZEOF_INT=4
So that definitely doesn't fly for e.g. i386/x86_64 universal builds.
If only the cudd portion of this build process has these assumptions about bit size, then we could write our own muniversal-esque build-and-lipo process just for the cudd part. But grep
ping the source for "NUSMV_SIZEOF
" does not give me the impression that this is the case. Otherwise, if also the minisat and the main nusmv parts have similar issues, we could use the muniversal portgroup, though we'd still need our own code to properly deal with running the pre-configure part for each architecture.
Change History (5)
comment:1 Changed 13 years ago by ryandesign (Ryan Carsten Schmidt)
comment:2 Changed 13 years ago by ryandesign (Ryan Carsten Schmidt)
Ok, in reading the various readme files in nusmv, I see that no, we cannot use the standalone libcudd port:
The CUDD library included in the NuSMV distribution must be used with NuSMV even if another version of the CUDD library is already installed in the system.
We also cannot use the standalone minisat port:
The current version of NuSMV is linked to minisat2-070721. Version minisat-2.2.0 requires features which are being developed in NuSMV, and which are not available in the official versions yet.
comment:4 Changed 8 years ago by mf2k (Frank Schima)
Owner: | mww@… deleted |
---|---|
Status: | new → assigned |
See #53012.
I see that we have a libcudd port. Could we use that instead of using the version included with nusmv? That might simplify things.