[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