[Bug 486757] Review Request: divine-mc - Multi-core model checking system for proving specifications
bugzilla at redhat.com
bugzilla at redhat.com
Wed Mar 18 09:42:47 UTC 2009
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=486757
--- Comment #13 from Milos Jakubicek <xjakub at fi.muni.cz> 2009-03-18 05:42:44 EDT ---
Yes, I had -- sorry for answering late but there were indeed some things I had
to clarify with Peter (upstream).
First of all, the install target of cmake doesn't install all the binaries it
should -- there should be following files installed into %{_bindir}:
./_build/tools/divine-mc.compile-pml
./_build/tools/divine-mc.combine
./_build/tools/divine-mc
./_build/tools/divine-mc.probabilistic
./_build/tools/divine-mc.simulate
This can be fixed by adding the missing into tools/CMakeLists.txt:install(
TARGETS divine-mc divine-mc.simulate DESTINATION bin ).
And now the real problem: I found the official site of Promela, see
http://wwwhome.cs.utwente.nl/~michaelw/nips/ (please use the tarball from there
as Source1), and as there are several projects using Promela I had to
reconsider the decision of including Promela into divine-mc. Moreover, one
should quote here what the guidelines say:
"Fedora packages should make every effort to avoid having multiple, separate,
upstream projects bundled together in a single package."
Well, unfortunately, this is now impossible. The jars are packed into one perl
script (divine-mc.compile-pml) and unpacked runtime. This is hard to bypass
without heavy code changes, but Peter agreed on making divine-mc independent on
Promela location in 2.0 version (upstream trac ticket placed under
http://anna.fi.muni.cz/divine/trac/ticket/14)
Would you agree on packaging Promela too (...I would review it) so that it
could be removed from divine-mc 2.0?
To sum it up:
* please fix the cmake install target, make sure that the Perl dependencies are
ok then, see:
https://fedoraproject.org/wiki/Packaging/Perl#Perl_Requires_and_Provides
* use upstreams tarball URL for Source1 (Promela), please add the link to the
trac ticket with the necessary explanation why it is not packaged separate now.
* regarding Java, the BR and R should be versioned, hence please use:
BuildRequires: java-devel >= 1:1.6.0
BuildRequires: ant
Requires: java >= 1:1.6.0
Requires: jpackage-utils
(BR: jpackage-utils is pulled by ant)
* regarding the following test:
# This one is omitted; it takes too long to be useful as a build test:
# ./_build/tools/divine-mc owcty examples/peterson-liveness.dve
You can surround this one with:
%if %{?_with_tests:1}%{!?_with_tests:0}
./_build/tools/divine-mc owcty examples/peterson-liveness.dve
%endif
so that one can run this test by passing "--with tests" to rpmbuild on demand.
* I would appreciate if you would submit the review request for Promela before
approving this package (the package and review shouldn't be problematic AFAIK).
I hope this is all...;)
--
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.
More information about the package-review
mailing list