Bug 592579 - Review Request: Frama-c - Framework for source code analysis of C software
Summary: Review Request: Frama-c - Framework for source code analysis of C software
Keywords:
Status: CLOSED RAWHIDE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
low
medium
Target Milestone: ---
Assignee: David A. Wheeler
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
: 564520 (view as bug list)
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2010-05-15 14:12 UTC by Mark Rader
Modified: 2012-08-01 09:58 UTC (History)
6 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of: 564520
Environment:
Last Closed: 2012-08-01 09:58:38 UTC
Type: ---
Embargoed:
dwheeler: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description Mark Rader 2010-05-15 14:12:20 UTC
Spec URL: http://tpath3.dnsalias.net/openproofs/frama-c.spec
SRPM URL: http://tpath3.dnsalias.net/openproofs/frama-c-1.4-1.fc12.src.rpm
Description:Frama-C is a suite of tools dedicated to the analysis of the
source
code of software written in C.

Frama-C gathers several static analysis techniques in a single
collaborative framework. The collaborative approach of Frama-C allows
static analyzers to build upon the results already computed by other
analyzers in the framework. Thanks to this approach, Frama-C provides
sophisticated tools, such as a slicer and dependency analysis.

There are 6 warnings.  3 deal with the QPL License with exceptions.  3 deal
with unstripped binaries.  At least one of the binaries is a loadable library
and can not be stripped.  I suspect the other two are also. 

This is an attempt to move the maintenance of this package from  Alan Dunn, and is done at his request.  This replaces bug 564520 and the people who are interested should read https://bugzilla.redhat.com/show_bug.cgi?id=564520 for more information.

Comment 1 Richard W.M. Jones 2010-05-15 16:28:40 UTC
*** Bug 564520 has been marked as a duplicate of this bug. ***

Comment 2 David A. Wheeler 2010-05-17 18:17:43 UTC
Thanks for doing this!!  I'll start reviewing, but I cannot serve as a sponsor.

Comment 3 David A. Wheeler 2010-05-21 22:27:06 UTC
My first step in reviewing the package was reviewing the rpmlint errors
from the spec file and the 2 generated binary RPMs,
which on my system produced 2 errors and 5 warnings.

I'd *really* like input from an OCaml expert (PSST: RICHARD JONES!)
for the "unstripped-binary-or-object" messages, esp. for
"/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs".  Ignoring that warning
is easy enough, but *should* it be ignored?

With that, here are some initial comments:

* frama-c.i586: E: devel-dependency gtksourceview-devel

You need to fix some "Requires:" lines in the .spec file.
In particular, the problem is that you've specifically included
as "Requires" statements some -devel libraries as "Requires".
You should *not* make "Requires" statements unless you have to;
rpm will figure them out, and will typically do a better job anyway.
The *big* case where you need requires statements is if you need
to state that specific version (minimums) are required.

So, please change the spec as follows, which improves the
spec and gets rid of this rpmlint error:
 
 Requires: graphviz >= 2.0.0
-Requires:   gtksourceview >= 1.0.0, gtksourceview-devel
-Requires:  ocaml >= 3.11.0, ocaml-findlib-devel, ocaml-lablgtk-devel, ocaml-ocamlgraph-devel
+Requires: gtksourceview >= 1.0.0
+Requires: ocaml >= 3.11.0
 


* frama-c.i586: W: invalid-license QPL with modifications
* frama-c-devel.i586: W: invalid-license QPL with modifications

The term "QPL with modifications" is not one of the valid licenses
known to rpmlint.  I looked into what's going on, and I think this
software license is clearly FLOSS, as I describe below.

However, you're going to have to get legal to approve it, as described in:
  http://fedoraproject.org/wiki/Packaging:LicensingGuidelines
"The License: field must be filled with the appropriate license Short
License identifier(s) from the "Good License" tables on the  Fedora
Licensing page. If your license does not appear in the tables, it needs to
be sent to fedora-legal-list (note that this list is moderated,
only members may directly post). If the license is approved, it will be
added to the appropriate table."

They'll also need to approve some sort of short name, since
"QPL with modifications" is not on the approved list.

I'm not a lawyer, but I *did* look at this, and here's what I learned
in the hope that it helps.  At issue seems to be this license:
 ~/rpmbuild/BUILD/frama-c-Beryllium-20090902/licenses/Q_MODIFIED_LICENSE

It's QPL version 1.0, an already-approved FLOSS license, with some
modifications.  I only found 2 modifications:
1. An *additional* permission.  If you DON'T release to your program
   to the general public, you don't have to comply with QPL requirement 6c.
   ("You must ensure that all modifications included in the
   machine-executable forms are available under the terms of this license.")
   I don't see how giving ADDITIONAL permissions makes a FLOSS license
   non-FLOSS.
2. A choice of venue ("This license is governed by the Laws of France.")
   I'm not crazy about choice-of-venue clauses, but other FLOSS licenses
   have them (e.g., CeCILL), so that cannot make it non-FLOSS.

Here's the actual text from the license that shows these modifications:
==============================================================
In the following, "the Library" refers to the following file:
  standard.mly
and "the Generator" refers to all files marked "Copyright INRIA" in the
root directory.

The Generator is distributed under the terms of the Q Public License
version 1.0 with a change to choice of law (included below).

The Library is distributed under the terms of the GNU Library General
Public License version 2 (included below).

As a special exception to the Q Public Licence, you may develop
application programs, reusable components and other software items
that link with the original or modified versions of the Generator
and are not made available to the general public, without any of the
additional requirements listed in clause 6c of the Q Public licence.

As a special exception to the GNU Library General Public License, you
may link, statically or dynamically, a "work that uses the Library"
with a publicly distributed version of the Library to produce an
executable file containing portions of the Library, and distribute
that executable file under terms of your choice, without any of the
additional requirements listed in clause 6 of the GNU Library General
Public License.  By "a publicly distributed version of the Library",
we mean either the unmodified Library as distributed by INRIA, or a
modified version of the Library that is distributed under the
conditions defined in clause 3 of the GNU Library General Public
License.  This exception does not however invalidate any other reasons
why the executable file might be covered by the GNU Library General
Public License.
... [at the end of the QPL]:
                            Choice of Law
This license is governed by the Laws of France.
==============================================================





* frama-c.i586: W: unstripped-binary-or-object /usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs
* frama-c.i586: W: unstripped-binary-or-object /usr/bin/frama-c.byte
* frama-c.i586: W: unstripped-binary-or-object /usr/bin/frama-c-gui.byte

I'm not an OCaml expert, and these are clearly related to OCaml.
I'd really like the input of an OCaml expert on this point.
For some guidance, I looked here:
  http://fedoraproject.org/wiki/Packaging/OCaml

Rpmlint reports "unstripped-binary-or-object" on /usr/bin/frama-c.byte
and /usr/bin/frama-c-gui.byte but I think it's even more complicated :-(.
Rpmlint correctly reports that it has a symbol table (readelf agrees).

However, trying to run these files reports "No bytecode file specified.",
a tell-tale sign of a (partly) *stripped* bytecode file.

Basically, these two ".byte" files are completely corrupted; they can't
be run as-is.  If this is unfixable, perhaps it'd be better to simply
remove these ".byte" files, since the cannot be run at all, and limit
the package to those architectures which support native executables.

This page:
  http://caml.inria.fr/pub/docs/manual-ocaml/libref/Dynlink.html
explains that .cmxs files are OCaml plugin files in native mode;
basically, they're libraries that can be dynamically loaded at run-time.
Suggestions welcome.


* frama-c.i586: E: forbidden-selinux-command-in-%post chcon
An rpmlint --info gives a little more info:
"A command which requires intimate knowledge about a specific SELinux
policy type was found in the scriptlet. These types are subject to change
on a policy version upgrade. Use the restorecon command which queries
the currently loaded policy for the correct type instead."

At issue is this text in the spec:
%post
chcon -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Ltl_to_acsl.cmxs'
semanage fcontext -a -t textrel_shlib_t '%{_libdir}frama-c/plugins/Ltl_to_acsl.cmxs'

You need to do this in a cleaner way; you're not supposed to use chcon
in %post.  You may find this useful:
 https://fedoraproject.org/wiki/PackagingDrafts/SELinux/PolicyModules



* BIG ISSUE: Where's the "-jessie" option of frama-c?

When I have a C file, I should be able to invoke:
 frama-c -jessie demo.c
yet "-jessie" isn't available.
I understand that the Jessie plug-in is actually in "Why",
but there needs to be a way to *invoke* it.


* Note: There's a newer version of Frama-C, version Boron 20100401,
  available on their site.  Should we switch to it?
  Obviously, there's an issue of how it invokes Jessie.

* I don't see your name ("Mark Rader") in the ChangeLog at the end.

Hope this helps...

Comment 4 Richard W.M. Jones 2010-05-22 06:32:29 UTC
Can you try stripping these binaries.  If they still work after
stripping, then we should ship them.  It's only a very old version
of the compiler where stripping bytecode binaries would break
them.

As for the license, the full license should be posted to
the fedora-legal mailing list, to get approval.

Comment 5 Richard W.M. Jones 2010-05-22 06:32:54 UTC
(In reply to comment #4)
> Can you try stripping these binaries.  If they still work after
> stripping, then we should ship them.

That is to say, we should ship them stripped.

Comment 6 David A. Wheeler 2010-05-22 18:41:32 UTC
The two *.byte files frama-c.byte and frama-c-gui.byte) don't work when generated using the *current* process.  Stripping them won't make them *better* :-).  If they can be fixed without much trouble, great, but otherwise, I don't think we should package non-working files, and we should package the files for the architectures where the OCaml compiler can produce machine code.  Most people won't notice the omission of the .byte files, since x86s are the most common architectures.

As for the license, I think it *MUST* be posted to fedora-legal, not merely a *should*.  But I have every expectation that it'll be approved.

Comment 7 Mark Rader 2010-05-23 03:55:13 UTC
David

On further investigation, the jessie issue appears to be more of a problem with why.  I will download the why source code and see if the jessie plugin gets installed with a source compile.

I have fixed the two errors.  The one with selinux mainly required substituting out a command.  All 3 files are now stripped so that is no longer a warning.

To be checked:

1.  Does everything still run.
2.  Legal issue.
3.  Is why supposed to install jessie.

Comment 8 Mark Rader 2010-05-23 15:28:49 UTC
I have checked the following:

1.  Everything runs with the files stripped.  So the spec version now strips all files.

2.  Why (compiled from source) installs the jessie plugins but even installed frama c does not seem to want to use them

Comment 9 Mark Rader 2010-05-23 16:09:53 UTC
I did a make clean on the why compile from source and now jessie seems to work.  Now the real issue is that jessie really comes from why not from frama c.  That being said, I begin to suspect that for proper operation the two need to be installed at the same time, and I suspect that they will need to be in the same package.

The next big issue is the legal one.

Comment 10 David A. Wheeler 2010-05-23 18:42:37 UTC
I don't think that "why" and "frama-c" need to be in the *same* package, but clearly some changes need to happen.  Sounds like you should just go ahead and package frama-c, and once done, we can modify why to depend on frama-c.  We *could* create a subpackage of why that includes Jessie (why-jessie), and just make *that* depend on frama-c, though it's not clear how many "why" users won't use jessie (if it's not many, it might be simpler to not split them up).

Comment 11 Mark Rader 2010-05-23 23:18:46 UTC
I have posted the new version for testing.

Comment 12 Richard W.M. Jones 2010-05-24 08:10:13 UTC
(In reply to comment #6)
> The two *.byte files frama-c.byte and frama-c-gui.byte) don't work when
> generated using the *current* process.  Stripping them won't make them *better*
> :-).  If they can be fixed without much trouble, great, but otherwise, I don't
> think we should package non-working files, and we should package the files for
> the architectures where the OCaml compiler can produce machine code.  Most
> people won't notice the omission of the .byte files, since x86s are the most
> common architectures.

There's a rule in the OCaml packaging guidelines that we should package
the best possible binaries only -- ie. native, if the platform supports
native compilation.  (And for a very long time, OCaml on Fedora's supported
architectures has always had native compilation).

(In reply to comment #9)
> I did a make clean on the why compile from source and now jessie seems to work.
>  Now the real issue is that jessie really comes from why not from frama c. 
> That being said, I begin to suspect that for proper operation the two need to
> be installed at the same time, and I suspect that they will need to be in the
> same package.

Generally, each source tarball should go in a separate SRPM.  There is a
packaging guideline rule for this too IIRC.

Comment 13 David A. Wheeler 2010-05-24 16:08:08 UTC
I'm looking over the .spec file for overall comments, before I delve into a point-by-point comparison with the guidelines.

* Every time you make a change you should bump the "Revision" number,
  and post the new URL.  That'll be *critical* when it's submitted to the
  repository, but it'd reduce confusion now too.
* Patch0 comment says:
  "The configure file uses graph.cmo in compiling a test program to
  check for ocamlgraph, but Fedora doesn't include this file in its
  distributions."
  I'm confused, there *is* an ocaml-ocamlgraph package.
  Is the Fedora respository's ocamlgraph the wrong (too old) version?
  Or, is this just an old comment based on an older version of this spec,
  now OBE?
* Patch1 isn't prefixed with "frama-c-", and that can cause trouble.
  In general, if someone looks in their rpmbuild/SOURCES, they can get
  confused (and namespace issues could result) if they aren't prefixed.
  You should  prefix the patch filenames with NAME- (e.g., "frama-c-").
* Rejected Debian Patch2 (0002-Make-Jessie-plugin-use-Jc-from-Why-2.19.patch)
  comment says, "I don't know why we would want to use that
  Jessie -> not including this patch".  You're not including that patch
  because we want to use a later version of Why, correct?  If so, just say:
  "We use a later version of Why, so this patch is irrelevant".
  Although I applaud "I don't know..." comments for their honesty, I think
  we should track them down so you can simply say why something was done.
  In this case, there's a good reason: The patch is for an obsolete
  version of "why".
* Rejected Debian patch "0003-Add-dGraphView.cmo-when-linking.patch"
  says "I'm not sure quite what this patch does, but I'm going to
  leave it out for now".  Need to track this down a little of what this is.
  My *guess* from the text is that it merges graphview into another
  another library, and we *don't* want to do that (because then upgrading
  graphview won't updated the merged file).  If that's the
  situation, please say so directly.
* Rejected Debian patch 0004-Use-GSourceView2.patch comment says
  "I didn't see any Fedora package providing the files that this patch
  references -> dropping for now".  
  Did you check out "gtksourceview2-devel" and "gtksourceview2"?
  It's possible that the patch includes the *OCaml* bindings for these
  and that Fedora doesn't include those bindings.  If so, just say that.
* In Patch "frama-c-1.4-ptests-fix-for-ocaml-3.11.2.patch" there
  needs to be a comment explaining (1) what it's for, and (2)
  when you submitted it upstream (and if not, why not).  Shouldn't be *long*,
  but it should say *something*.
* Nit: Your "Requires:" statements have inconsistent indenting.
  Please fix while you're at it.
* Nit: "plug in's" is not a word.  An "'s" is either a possessive or
  an appreviation of "is", and this is neither (it's just a plural).
  I'd suggest "plug-ins" instead.  If the spellchecker whines, too bad.
* I notice that the entire "%check" section is commented out.
  A %check section is NOT required, and I'd prefer the comments to nothing,
  but it'd be nice if it worked :-).
* As noted earlier, the .byte files don't work, and probably shouldn't
  be packaged at all.
* I'll check the %files list separately.
* In %post, just remove the comment:
  #chcon -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Ltl_to_acsl.cmxs'
  I don't see that the commend adds anything.
* The %changelog doesn't list "Mark Rader"; it should!

Comment 14 David A. Wheeler 2010-05-24 17:50:49 UTC
The updated rpm fails on 32-bit systems.  You have a built-in assumption that there is a "lib64", but on 32-bit system it's just "lib".  Here's the error:
cp -f man/frama-c.1 /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/share/man/man1/frama-c-gui.1
for plugin in ; do \
	  MAKEFLAGS="" make FRAMAC_LIBDIR=/home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/lib/frama-c FRAMAC_SHARE=/home/dwheeler/rpmbuild/BUILD/frama-c-Beryllium-20090902/share -C $plugin install; \
	done
+ strip /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/bin/frama-c
+ strip /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/bin/frama-c-gui
+ strip /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/bin/frama-c.byte
+ strip /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/bin/frama-c-gui.byte
+ strip /home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/lib64/frama-c/plugins/Ltl_to_acsl.cmxs
strip: '/home/dwheeler/rpmbuild/BUILDROOT/frama-c-1.4-1.fc11.i386/usr/lib64/frama-c/plugins/Ltl_to_acsl.cmxs': No such file
error: Bad exit status from /var/tmp/rpm-tmp.TXN0rD (%install)

Can you fix this soon?

Although I haven't looked in detail at the packaging of "why", I suspect it'd be fairly easy to create a new subpackage "why-jessie"; the new subpackage would include Jessie and the Jessie plug-in, and depend on frama-c.  I think that would accurately reflect the situation.  Jessie is delivered as part of the source code of "why", you can use other parts of "why" without using Jessie, but Jessie requires the use of frama-c (to create its data format and the drop-in location for its plug-in).  That shouldn't be hard to do once the "frama-c" package is in the repository.

Go ahead and package the Frama-C version you're using.  I hope that in the not-to-distant future you'll update this package to the just-released new version, but I understand that it's easier to not change versions midstream.  And I don't know who's had experience with the newly-released version; it might be best to wait a little bit, until any problems have been shaken out, before updating the package.

Comment 15 Mark Rader 2010-05-24 18:36:38 UTC
I should have this one fixed soon, I will probably get it fixed tonight.  I will also be able to address some of the ones listed in the previous error report.

Comment 16 David A. Wheeler 2010-05-24 18:39:51 UTC
Here are the guidelines from:
 http://fedoraproject.org/wiki/Packaging:ReviewGuidelines
It's hard for me to check on some of these until it can once again build binary
packages on all expected architectures, but I thought it'd be helpful to do as
much as I can now.  In that spirit, here are my comments:

    *  MUST: rpmlint must be run on every package. The output should be posted
in the review.[1]

IN PROGRESS.  rpmlint output shown earlier, and issues being worked on.

    * MUST: The package must be named according to the Package Naming
Guidelines .

OK

    * MUST: The spec file name must match the base package %{name}, in the
format %{name}.spec unless your package has an exemption. [2] .

OK

    * MUST: The package must meet the Packaging Guidelines .

OK generally, but see other comments (including this one).

    * MUST: The package must be licensed with a Fedora approved license and
meet the Licensing Guidelines .

IN PROGRESS.  I suspect the license is fine, but it *must* be specifically
approved.

    * MUST: The License field in the package spec file must match the actual
license. [3]
Spec claims:
License:        LGPLv2 and GPL+ and GPLv2 and GPLv2+ and BSD and (QPL with
modifications)

See the previous threads about the licensing of this.
I did some additional checking.

In particular: I didn't see any examples of "GPL+", only GPLv2 and GPLv2+.  If
there are no source programs with GPL+, then "GPL+" should be removed from the
license list.  Did I miss it somehow?  If so, what file is "GPL+"?

Here's what I found when I looked:

Under the "src" directory I spot-checked the ".ml" and ".c" files, and they
were
all LGPL v2.1.  Same for "share" and "ptests".

The "cil" subdirectory has "LICENSE", which is (3-clause) BSD, and that matches
the .ml files under there.

external/ptmap.ml has the "Q modified license", so it *IS* used.

./tests/spec/purse.c: GPLv2 (*NOT* GPLv2+, but strictly GPLv2)
./tests/idct/idct.c: GPLv2+
./tests/idct/ieee_1180_1990.c: GPLv2+

The "licenses" directory contains this:
 GPLv3  LGPLv2.1  LGPLv3  Q_MODIFIED_LICENSE
The Q_MODIFIED_LICENSE includes the "Q modified license" and
a reference to "LGPLv2".
This *DIRECTORY* includes GPLv3, but I did not find ANY source file
that actually referred to GPLv3.  A few referred to GPLv2+,
but the license text should say "GPLv2+" and not "GPLv3".
So, even though there's a "GPLv3" in the "licenses" directory,
you should not add "GPLv3" to the Licenses entry.


    * MUST: If (and only if) the source package includes the text of the
license(s) in its own file, then that file, containing the text of the
license(s) for the package must be included in %doc.[4]

FAIL.  Under %files, need to add entries for the license files that are there.

    * MUST: The spec file must be written in American English. [5]

OK

    * MUST: The spec file for the package MUST be legible. [6]

OK

    * MUST: The sources used to build the package must match the upstream
source, as provided in the spec URL. Reviewers should use md5sum for this task.
If no upstream URL can be specified for this package, please see the Source URL
Guidelines for how to deal with this.

OK - hashes match.

wget http://frama-c.com/download/frama-c-Beryllium-20090902.tar.gz
 sha512sum frama-c-Beryllium-20090902.tar.gz
~/rpmbuild/SOURCES/frama-c-Beryllium-20090902.tar.gz 
1f78aaaf99f62a5746a4e673a722d9384156d29027d3ca079c4f0d0de9afa4c4aacd6b65721375f094698453ed339b9de9f91a2ca2d41d4c5784390b0eccb0e3
 frama-c-Beryllium-20090902.tar.gz
1f78aaaf99f62a5746a4e673a722d9384156d29027d3ca079c4f0d0de9afa4c4aacd6b65721375f094698453ed339b9de9f91a2ca2d41d4c5784390b0eccb0e3
 /home/dwheeler/rpmbuild/SOURCES/frama-c-Beryllium-20090902.tar.gz


    * MUST: The package MUST successfully compile and build into binary rpms on
at least one primary architecture. [7]

IN PROGRESS.

    * MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in
bugzilla, describing the reason that the package does not compile/build/work on
that architecture. The bug number MUST be placed in a comment, next to the
corresponding ExcludeArch line. [8]

FAIL - need to add those.

    * MUST: All build dependencies must be listed in BuildRequires, except for
any that are listed in the exceptions section of the Packaging Guidelines ;
inclusion of those as BuildRequires is optional. Apply common sense.

Nothing obviously wrong, but need to check with Mock.

    * MUST: The spec file MUST handle locales properly. This is done by using
the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9]

NA; no locale info.

    * MUST: Every binary RPM package (or subpackage) which stores shared
library files (not just symlinks) in any of the dynamic linker's default paths,
must call ldconfig in %post and %postun. [10]

NA.

    * MUST: Packages must NOT bundle copies of system libraries.[11]

ISSUE.  This has its own version of cil, yet there is an ocaml-cil.

    * MUST: If the package is designed to be relocatable, the packager must
state this fact in the request for review, along with the rationalization for
relocation of that specific package. Without this, use of Prefix: /usr is
considered a blocker. [12]

NA

    * MUST: A package must own all directories that it creates. If it does not
create a directory that it uses, then it should require a package which does
create that directory. [13]

TODO: Looks okay, will be easier to check when it builds... :-).

    * MUST: A Fedora package must not list a file more than once in the spec
file's %files listings. [14]

TODO: Will wait to check til it builds.

    * MUST: Permissions on files must be set properly. Executables should be
set with executable permissions, for example. Every %files section must include
a %defattr(...) line. [15]

Will wait to check til it builds.

    * MUST: Each package must consistently use macros. [16]
OK

    * MUST: The package must contain code, or permissable content. [17]

OK

    * MUST: Large documentation files must go in a -doc subpackage. (The
definition of large is left up to the packager's best judgement, but is not
restricted to size. Large can refer to either size or quantity). [18]
NA

    * MUST: If a package includes something as %doc, it must not affect the
runtime of the application. To summarize: If it is in %doc, the program must
run properly if it is not present. [18]

NA/FAIL.  Nothing is marked as %doc, but I think that's a mistake.

    * MUST: Header files must be in a -devel package. [19]
ISSUE.  This is *primarily* an application-level program, but it provides OCaml
headers for plug-ins, yes?  Shouldn't those be separate?

    * MUST: Static libraries must be in a -static package. [20]
NA

    * MUST: If a package contains library files with a suffix (e.g.
libfoo.so.1.1), then library files that end in .so (without suffix) must go in
a -devel package. [19]

TODO: Waiting for working package.

    * MUST: In the vast majority of cases, devel packages must require the base
package using a fully versioned dependency: Requires: %{name} =
%{version}-%{release} [21]
NA (today)

    * MUST: Packages must NOT contain any .la libtool archives, these must be
removed in the spec if they are built.[20]
TODO: Wait for build

    * MUST: Packages containing GUI applications must include a %{name}.desktop
file, and that file must be properly installed with desktop-file-install in the
%install section. If you feel that your packaged GUI application does not need
a .desktop file, you must put a comment in the spec file with your explanation.
[22]
FAIL.

Need a desktop file.  These are easy to create.  For a trivial example see:
 gwhy.desktop
from "why".

    * MUST: Packages must not own files or directories already owned by other
packages. The rule of thumb here is that the first package to be installed
should own the files or directories that other packages may rely upon. This
means, for example, that no package in Fedora should ever share ownership with
any of the files or directories owned by the filesystem or man package. If you
feel that you have a good reason to own a file or directory that another
package owns, then please present that at package review time. [23]

TODO: Will check once it's building.

    * MUST: All filenames in rpm packages must be valid UTF-8. [24]
TODO: Will check once it's building.

I'll get to the SHOULD items after it builds.

Comment 17 Mark Rader 2010-05-25 14:30:04 UTC
There is an updated version of the bug source.

Spec URL: http://tpath3.dnsalias.net/openproofs/frama-c.spec
SRPM URL: http://tpath3.dnsalias.net/openproofs/frama-c-1.4-2.fc12.src.rpm
Description:Frama-C is a suite of tools dedicated to the analysis of the
source code of software written in C.

I have excluded the .byte files.  It should now compile correctly on the 64 and 32 bit platforms.

Comment 18 Richard W.M. Jones 2010-05-25 14:33:18 UTC
Can I suggest you do a scratch build in Koji, ie:

koji build --scratch dist-f14 frama-c-1.4-2.fc12.src.rpm

Comment 19 David A. Wheeler 2010-05-25 17:54:23 UTC
Thanks, I'm now looking over the updated 1.4-2 version.  Much progress, but a few more things to do.

The rpmbuild now works on 32-bit x86, and "rpmlint" is now much happier compared to 2 versions ago.  I did:
  rpmlint frama-c.spec ../RPMS/i586/frama-c-*-2.* ../SRPMS/frama-c-1.4-2.fc11.src.rpm
The only rpmlint reports involve the license, which you're already addressing with fedora legal:
frama-c.i586: W: invalid-license QPL with modifications
frama-c-devel.i586: W: invalid-license QPL with modifications
frama-c.src: W: invalid-license QPL with modifications
3 packages and 1 specfiles checked; 0 errors, 3 warnings.

I don't understand why this package installs "/usr/bin/ptests.byte".
I don't think that is a user-level program; I believe that is just
a test program that should be *used* during a "make check" as part of the build.
Thus, I think you should NOT install that program as part of this package.


Based on comment #3:
* All rpmlint errors are gone, except for the licensing issues being addressed.
  There's no longer a "chcon" command (inc. the unneeded comment)
* The "-jessie" option will require a change to "why" after
  frama-c enters the repository, so that's addressed.
* I see your name ("Mark Rader") in the ChangeLog at the end, good!
  Usually there's a blank line between major entries (E.g., between leading "*"),
  you probably should add that.

Regarding comment #6 and comment #12:
* Excluding the ".byte" files is fine.  But that means that this package won't work on some architectures, so you need some ExcludeArch statements.


Regarding comment #13:
* Revision number bumped, good! Thanks.
* I *still* don't understand this comment:
  "The configure file uses graph.cmo in compiling a test program to
  check for ocamlgraph, but Fedora doesn't include this file in its
  distributions."

  But Fedora *does* include the ocaml-ocamlgraph package, and that
  package specifically installs "/usr/lib/ocaml/ocamlgraph/graph.cmo".
  So I really don't understand what this spec is trying to say.
  (I realize that you inherited this package from others, so this is probably
  inherited as well, but it sure isn't clear as it is.)

* I really think you should prefix the filename of Patch1 with "frama-c-".

  Otherwise, if someone builds many packages inside a shared rpmbuild/SOURCES
  directory, there's a (tiny) risk that this will overlap with something else.
  The risk is tiny, but better to avoid the question.

* Patch2 (ptests) has *no* explanation, and that is NOT okay.
  Need to briefly explain what it does, and either (1) when it was sent
  upstream, or (2) why it wasn't sent upstream.  I believe that is a MUST.

* Nit: "plug in's" is still not a word.  An "'s" is either a possessive or
  an appreviation of "is", and this is neither (it's just a plural).
  I'd suggest "plug-ins" instead.  If the spellchecker whines, too bad.

* No %check section.  It's not required, but it'd be nice if it worked.
  In the long term, a %check section - even one with just one trivial test -
  will catch problems like silently failed builds.

* I'll check the %files list separately.


You really need to do a Koji build (see comment #18).  I can't do that this at this moment from where I am (due to SSL munging where I am), but I did "mock --rebuild" on 32-bit, and found a problem that Koji would have found.  I think you're missing a BuildRequires.  When I use mock --rebuild, I get:
 ocamlc.opt -o lib/gui/Scope.cmo -w Ael -warn-error A -annot   -g -I src/misc -I src/ai -I src/memory_state -I src/toplevel -I src/slicing_types -I src/pdg_types -I src/kernel -I src/logic -I src/lib -I src/project -I src/buckx -I src/gui -I external -I cil/src -I cil/src/ext -I cil/src/frontc -I cil/src/logic -I cil/ocamlutil -I lib/plugins -I lib  -I +ocamlgraph  ........
 /usr/bin/ld: cannot find -lgnomecanvas-2
 collect2: ld returned 1 exit status
 File "_none_", line 1, characters 0-1:
 Error: Error while building custom runtime system

In short, the build is complaining that there is no library gnomecanvas-2.  A quick "rpm -qf /usr/lib/libgnomecanvas-2.so" suggests to me that you need to add this to the spec file:
 BuildRequires: libgnomecanvas-devel

Once I added that "BuildRequires: libgnomecanvas-devel", the mock build worked for me.  You should still do a Koji build, since that will detect problems on many architectures.  (Be sure to add ExcludeArch's first; we already know that this package will NOT work on some other architectures because it doesn't generate proper .byte files.)

As noted in "How to create an RPM package", I've found it to be very helpful to "yum install auto-buildrequires" and then run "auto-br-rpmbuild -ba SPECFILE". Unfortunately, it didn't seem to be enlightening in this case.



Per comment #16, here are the previously-unresolved guidelines:
*  MUST: rpmlint must be run on every package. The output should be posted
in the review.[1]

IN PROGRESS.  rpmlint output shown earlier, and issues being worked on.

* MUST: The package must meet the Packaging Guidelines .

OK generally, but see other comments (including this one).

* MUST: The package must be licensed with a Fedora approved license and
meet the Licensing Guidelines .

IN PROGRESS.  I suspect the license is fine, but it *must* be specifically
approved.

* MUST: The License field in the package spec file must match the actual
license. [3]

FAIL.  The "License" says "GPL+".  I found "GPLv2+", but no "GPL+".
I think you should remove the "GPL+", or find out why it's there.


* MUST: If (and only if) the source package includes the text of the
license(s) in its own file, then that file, containing the text of the
license(s) for the package must be included in %doc.[4]

FAIL.  Under %files, need to add entries for the license files that are there. E.G.:
 %doc licenses/LGPLv2.1
 %doc licenses/LGPLv3
 %doc licenses/Q_MODIFIED_LICENSE
 %doc cil/LICENSE


* MUST: The package MUST successfully compile and build into binary rpms on
at least one primary architecture. [7]

IN PROGRESS.  Need to add at least one BuildRequires.  You should test with Koji.

    * MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in
bugzilla, describing the reason that the package does not compile/build/work on
that architecture. The bug number MUST be placed in a comment, next to the
corresponding ExcludeArch line. [8]

FAIL.  Need to add ExcludeArch info.


    * MUST: All build dependencies must be listed in BuildRequires, except for
any that are listed in the exceptions section of the Packaging Guidelines ;
inclusion of those as BuildRequires is optional. Apply common sense.

FAIL.  See below about Koji, BuildRequires.

    * MUST: Packages must NOT bundle copies of system libraries.[11]

ISSUE.  This has its own version of cil, yet there is an ocaml-cil.
Need to at least document this in the spec file.  Since upstream has
forked their own version of cil, I don't see any way around this :-(,
but you need to include a reasonable justification in the spec comments.


    * MUST: A package must own all directories that it creates. If it does not
create a directory that it uses, then it should require a package which does
create that directory. [13]

OK.

    * MUST: A Fedora package must not list a file more than once in the spec
file's %files listings. [14]

FAIL.  These files are in the main package *AND* in the -devel package:
/usr/share/man/man1/frama-c.1.gz
/usr/share/man/man1/frama-c-gui.1.gz

You can find duplicates by doing:
 cd ~/rpmbuild/RPMS/ARCH # Substitute "ARCH" for your architecture
 rpm -qlp frama-c-1.4-2.fc11.*.rpm | sort > ,1
 rpm -qlp frama-c-devel-1.4-2.fc11.*.rpm | sort > ,2
 comm -12 ,1 ,2

    * MUST: Permissions on files must be set properly. Executables should be
set with executable permissions, for example. Every %files section must include
a %defattr(...) line. [15]

OK.

    * MUST: If a package includes something as %doc, it must not affect the
runtime of the application. To summarize: If it is in %doc, the program must
run properly if it is not present. [18]

NA/FAIL.  Nothing is marked as %doc, but I think that's a mistake.

    * MUST: Header files must be in a -devel package. [19]
ISSUE.  This is *primarily* an application-level program, but it provides OCaml
headers for plug-ins, yes?  Shouldn't those be separate?

    * MUST: If a package contains library files with a suffix (e.g.
libfoo.so.1.1), then library files that end in .so (without suffix) must go in
a -devel package. [19]

NA.  No ".so.SUFFIX" files.

    * MUST: Packages must NOT contain any .la libtool archives, these must be
removed in the spec if they are built.[20]

OK.  There aren't any.

    * MUST: Packages containing GUI applications must include a %{name}.desktop
file, and that file must be properly installed with desktop-file-install in the
%install section. If you feel that your packaged GUI application does not need
a .desktop file, you must put a comment in the spec file with your explanation.
[22]

FAIL.

You need a desktop file - that way, users can access the GUI from their graphical menu.  These are easy to create.  For a trivial example see:
 gwhy.desktop
from "why".

Once you create a nice .desktop file, you need to submit it to upstream so that they'll include it in the future.  The .desktop spec is now widely used (GNOME and KDE use them in particular), and they make GUI users happy :-).


    * MUST: Packages must not own files or directories already owned by other
packages. The rule of thumb here is that the first package to be installed
should own the files or directories that other packages may rely upon. This
means, for example, that no package in Fedora should ever share ownership with
any of the files or directories owned by the filesystem or man package. If you
feel that you have a good reason to own a file or directory that another
package owns, then please present that at package review time. [23]

OK

    * MUST: All filenames in rpm packages must be valid UTF-8. [24]

OK.  I tested with this, and there were no errors:
 rpmls ../RPMS/i586/frama-c-*-2* | iconv -f utf-8 -t utf-8




As promised, here are the SHOULDs:

#  SHOULD: If the source package does not include license text(s) as a separate file from upstream, the packager SHOULD query upstream to include it. [25]

NA.  There are separate license files.

# SHOULD: The description and summary sections in the package spec file should contain translations for supported Non-English languages, if available. [26]

Nice-to-have, but not required.  Unless you can easily translate the text to another language, carry on.

# SHOULD: The reviewer should test that the package builds in mock. [27]

OK.  I did that, as described earlier, and found a missing BuildRequire.

# SHOULD: The package should compile and build into binary rpms on all supported architectures. [28]

Won't happen.  As it is, it'll only work on systems where the OCaml compiler generates machine code.  Maybe in the future?

# SHOULD: The reviewer should test that the package functions as described. A package should not segfault instead of running, for example.

OK.  I tried out the GUI, and it came up.

# SHOULD: If scriptlets are used, those scriptlets must be sane. This is vague, and left up to the reviewers judgement to determine sanity. [29]

OK.  A very short (2-line) scriptlet is included; looks sane to me.

# SHOULD: Usually, subpackages other than devel should require the base package using a fully versioned dependency. [21]

NA

# SHOULD: The placement of pkgconfig(.pc) files depends on their usecase, and this is usually for development purposes, so should be placed in a -devel pkg. A reasonable exception is that the main pkg itself is a devel tool not installed in a user runtime, e.g. gcc or gdb. [30]

NA.  No .pc files.

# SHOULD: If the package has file dependencies outside of /etc, /bin, /sbin, /usr/bin, or /usr/sbin consider requiring the package which provides the file instead of the file itself. [31]

NA.

# SHOULD: your package should contain man pages for binaries/scripts. If it doesn't, work with upstream to add them where they make sense.[32]

OK.  The man pages are included in *both* the main and -devel package, and they
should only be in the *main* package.

Comment 20 Mark Rader 2010-06-06 16:47:50 UTC
David 

I really think you should prefix the filename of Patch1 with "frama-c-".

Otherwise, if someone builds many packages inside a shared rpmbuild/SOURCES
directory, there's a (tiny) risk that this will overlap with something else.
The risk is tiny, but better to avoid the question.

Done

FAIL.  The "License" says "GPL+".  I found "GPLv2+", but no "GPL+".
I think you should remove the "GPL+", or find out why it's there.

removed

FAIL.  Under %files, need to add entries for the license files that are there.
E.G.:
 %doc licenses/LGPLv2.1
 %doc licenses/LGPLv3
 %doc licenses/Q_MODIFIED_LICENSE
 %doc cil/LICENSE

done

FAIL.  These files are in the main package *AND* in the -devel package:
/usr/share/man/man1/frama-c.1.gz
/usr/share/man/man1/frama-c-gui.1.gz

You can find duplicates by doing:
 cd ~/rpmbuild/RPMS/ARCH # Substitute "ARCH" for your architecture
 rpm -qlp frama-c-1.4-2.fc11.*.rpm | sort > ,1
 rpm -qlp frama-c-devel-1.4-2.fc11.*.rpm | sort > ,2
 comm -12 ,1 ,2

done

Comment 21 Mark Rader 2010-06-06 17:53:34 UTC
David

I don't understand why this package installs "/usr/bin/ptests.byte".
I don't think that is a user-level program; I believe that is just
a test program that should be *used* during a "make check" as part of the
build.
Thus, I think you should NOT install that program as part of this package.

Now excluded

* I *still* don't understand this comment:
  "The configure file uses graph.cmo in compiling a test program to
  check for ocamlgraph, but Fedora doesn't include this file in its
  distributions."

Well it turns out that the extension changed from .cmo to .cam  so the patch fixes that change in extension.

Mark

Comment 22 Mark Rader 2010-06-06 18:32:13 UTC
David

I did a koji test run and it builds for FC 12 it bombs for FC and greater.  Complains that it can not find a patch.  I will try and puzzle it out for now this is the results.

Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2233753
None
Watching tasks (this may be safely interrupted)...
2233753 build (dist-f12, frama-c-1.4-3.fc12.src.rpm): free
2233753 build (dist-f12, frama-c-1.4-3.fc12.src.rpm): free -> open (x86-06.phx2.fedoraproject.org)
  2233754 buildArch (frama-c-1.4-3.fc12.src.rpm, ppc): open (ppc04.phx2.fedoraproject.org)
  2233756 buildArch (frama-c-1.4-3.fc12.src.rpm, ppc64): free
  2233755 buildArch (frama-c-1.4-3.fc12.src.rpm, x86_64): free
  2233757 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): free
  2233755 buildArch (frama-c-1.4-3.fc12.src.rpm, x86_64): free -> open (x86-02.phx2.fedoraproject.org)
  2233756 buildArch (frama-c-1.4-3.fc12.src.rpm, ppc64): free -> open (ppc04.phx2.fedoraproject.org)
  2233757 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): free -> open (x86-03.phx2.fedoraproject.org)
  2233757 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): open (x86-03.phx2.fedoraproject.org) -> closed
  0 free  4 open  1 done  0 failed
  2233755 buildArch (frama-c-1.4-3.fc12.src.rpm, x86_64): open (x86-02.phx2.fedoraproject.org) -> closed
  0 free  3 open  2 done  0 failed

Comment 23 Mark Rader 2010-06-06 20:51:29 UTC
David

Well everything now builds up to Fedora Core 14.  The output from Koji is as follows.

[rader@tpath3 SRPMS]$ koji build --scratch dist-f14 frama-c-1.4-3.fc12.src.rpm 
Uploading srpm: frama-c-1.4-3.fc12.src.rpm
[====================================] 100% 00:01:16  18.84 MiB 251.69 KiB/sec
Created task: 2233790
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2233790
None
Watching tasks (this may be safely interrupted)...
2233790 build (dist-f14, frama-c-1.4-3.fc12.src.rpm): free
2233790 build (dist-f14, frama-c-1.4-3.fc12.src.rpm): free -> open (x86-04.phx2.fedoraproject.org)
  2233792 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): free
  2233791 buildArch (frama-c-1.4-3.fc12.src.rpm, x86_64): open (x86-04.phx2.fedoraproject.org)
  2233792 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): free -> open (xb-01.phx2.fedoraproject.org)
  2233791 buildArch (frama-c-1.4-3.fc12.src.rpm, x86_64): open (x86-04.phx2.fedoraproject.org) -> closed
  0 free  2 open  1 done  0 failed
  2233792 buildArch (frama-c-1.4-3.fc12.src.rpm, i686): open (xb-01.phx2.fedoraproject.org) -> closed
  0 free  1 open  2 done  0 failed
2233790 build (dist-f14, frama-c-1.4-3.fc12.src.rpm): open (x86-04.phx2.fedoraproject.org) -> closed
  0 free  0 open  3 done  0 failed

2233790 build (dist-f14, frama-c-1.4-3.fc12.src.rpm) completed successfully

So we are well on the way with the technical part.

Comment 24 Mark Rader 2010-06-08 00:21:34 UTC
Spec URL: http://tpath3.dnsalias.net/openproofs/frama-c.spec
SRPM URL: http://tpath3.dnsalias.net/openproofs/frama-c-1.4-3.fc12.src.rpm
Description:Frama-C is a suite of tools dedicated to the analysis of the
source code of software written in C.

I have corrected a large number of issues pointed out by the reviewer.  The program should now produce a desktop entry.

Comment 25 David A. Wheeler 2010-06-08 01:47:52 UTC
Hooray!  Here are some quick comments from reviewing the .spec file:

Don't include no-value comments; most reviewers like .spec files to be short.  Please remove these lines (they're all obvious in context):
#  General Information
#Build Requires Section
#Requires Section
#Arcitecure Section

This still has "plug in's", which isn't correct English.  Please use "plug-ins" or "plug ins".

Thanks for creating the "frama-c-1.4-licensing" file.  The licensing issues were complicated, so documenting them in one place is a real plus.

I'm glad to see the .desktop file, that's important.

The changelog at the bottom has date/time/who, but doesn't say WHAT changed.
The changelog should list, for each new version, at least one change (if there were many, list the more important ones).  Thus, I would expect to see something like this:
* Sun Jun 06 2010 Mark Rader <msrader> 1.4-3
- Added documentation to explain the various licensing entries.
- Added .desktop file

* Wed May 24 2010 Mark Rader <msrader> 1.4-2
- Add SELinux context settings.

* Wed Feb 10 2010 Alan Dunn <amdunn> 1.4-1
- Initial Fedora RPM

Comment 26 David A. Wheeler 2010-06-08 01:53:49 UTC
You should submit your .desktop entry file upstream, and record in a  .spec file comment when you submitted it.  We want upstream to include and maintain the desktop entries (including translations), so that they're accurate/useful.  It'll also increase the likelihood that other distros will include a .desktop entry, and that they'll be consistent, which is good for everyone.

Comment 27 David A. Wheeler 2010-06-09 17:43:31 UTC
Hmm, I'm encountering a weird error on a 32-bit Fedora 13 system.  I'm not sure if the problem is with your package or my system (which I just upgraded).  Perhaps you'll see the obvious.

I did an rpmbuild on a 32-bit Fedora 13 system, which succeeded.  However, I could not install the resulting RPM with "rpm -i".  Error was:
rpm -i ./frama-c-1.4-3.fc13.i686.rpm 
error: Failed dependencies:
	ocaml(GtkSourceView_types) = 54a715ab00f97f086ec8efa5bdfb1079 is needed by frama-c-1.4-3.fc13.i686
	ocaml(Ltlast) = 74c3c642418d942308d59a8ee1249892 is needed by frama-c-1.4-3.fc13.i686
	ocaml(Promelaast) = ca8d09a78cd4262a60715d5b1b444b13 is needed by frama-c-1.4-3.fc13.i686

Erasing and re-installing "ocaml-lablgtk-devel ocaml-ocamlgraph-devel gtksourceview gtksourceview-devel", followed by another rpmbuild, did not help.  It's true that "is not installed" is returned from rpm -qi 'ocaml(GtkSourceView_types)' or the other two.  I don't see such packages, and "yum install 'ocaml(GtkSourceView_types)'" fails.

The only rpmlint error now is on the QPL license, and that's good news!

Comment 28 David A. Wheeler 2010-06-09 19:02:46 UTC
FYI: I'm installing a completely-clean Fedora 13 32-bit system for testing.  If the package works there, then I know that there's a problem in my newly-upgraded system.

Comment 29 David A. Wheeler 2010-06-09 21:47:56 UTC
Sorry, this FAILS to install on Fedora 13, 32-bit.

I did a complete clean from-scratch install of Fedora 13, "yum update"d everything, and built this package.  The building works, but when I try to install on 32-bit, I still get:

rpm -i ./frama-c-1.4-3.fc13.i686.rpm 
error: Failed dependencies:
 ocaml(GtkSourceView_types) = 54a715ab00f97f086ec8efa5bdfb1079 is needed by
frama-c-1.4-3.fc13.i686
 ocaml(Ltlast) = 74c3c642418d942308d59a8ee1249892 is needed by
frama-c-1.4-3.fc13.i686
 ocaml(Promelaast) = ca8d09a78cd4262a60715d5b1b444b13 is needed by
frama-c-1.4-3.fc13.i686

Comment 30 David A. Wheeler 2010-06-10 00:25:44 UTC
Here's some more info that may help you track down the problem on 32-bit x86 platforms.

Fedora 11 has basically the same problem, that is, it builds but does not install on 32-bit Fedora 11.  The error message there is different; when you attempt to "rpm -i", the error is:
/usr/sbin/semanage: File context for /usr/libframa-c/plugins/Ltl_to_acsl.cmxs already defined
restorecon:  stat error on /usr/libframa-c/plugins/Ltl_to_acsl.cmxs:  No such file or directory
warning: %post(frama-c-1.4-3.fc11.i586) scriptlet failed, exit status 255

Note that it reports on "/usr/libframa-c" instead of "/usr/lib/frama-c"; there's a missing "/" between "lib" and "frama-c".  That might be a clue.

I also tried rebuilding on 32-bit Fedora 13 after removing this:
 %if 0%{?fedora} >= 13
 %patch2 -p1
 %endif
on the theory that since this was specific to Fedora 13+, it might be the problem.  No dice; it won't compile without that patch.

Hope that info helps.

Comment 31 David A. Wheeler 2010-06-11 03:53:57 UTC
Here's more info that may help you.  Here's more on Fedora 11, 32-bit.

On Fedora 11 I changed the %post section to re-insert the missing "/", like this:
%post
semanage fcontext -a -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Ltl_to_acsl.cmxs'
restorecon -v '%{_libdir}/frama-c/plugins/Ltl_to_acsl.cmxs'

When I do "rpm -i ../RPMS/i586/frama-c-1.4-3.fc11.i586.rpm" it now complains:
restorecon reset /usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs context system_u:object_r:lib_t:s0->system_u:object_r:textrel_shlib_t:s0

But it *does* install on Fedora 11 once that change is made.

Comment 32 David A. Wheeler 2010-06-28 17:55:24 UTC
After looking further at this, I think that the license is a non-issue.

Comment 3 notes that this software uses the QPL.  The QPL is, of course, an already-approved FLOSS license.  There are only two modifications, and both cannot possibly affect whether or not it's FLOSS:
1. An *additional* permission.  If you DON'T release to your program
   to the general public, you don't have to comply with QPL requirement 6c.
   ("You must ensure that all modifications included in the
   machine-executable forms are available under the terms of this license.")
   Giving ADDITIONAL permissions can't make a FLOSS license non-FLOSS.
2. A choice of venue ("This license is governed by the Laws of France.")
   I'm not crazy about choice-of-venue clauses, but other FLOSS licenses
   have them; some even specifically use French jurisdiction (e.g., CeCILL).
   So that cannot make the software non-FLOSS either.

Therefore, this software is FLOSS as well.  At least, that's how I see it.  Comments welcome!  I wish legal had responded, but they *still* haven't, and in this case the answer seems crystal clear.

Comment 33 Mark Rader 2010-07-05 15:48:10 UTC
Spec URL: http://tpath3.dnsalias.net/openproofs/frama-c.spec
SRPM URL: http://tpath3.dnsalias.net/openproofs/frama-c-1.4-4.fc12.src.rpm
Description:Frama-C is a suite of tools dedicated to the analysis of the
source code of software written in C.

I have corrected a large number of issues pointed out by the reviewer.  The
program should now produce a file that will install on FC-13.  After running RPMLINT I get:

rpmlint frama-c.spec ../SRPMS/frama-c-1.4-4.fc12.src.rpm ../RPMS/x86_64/frama-c-1.4-4.fc12.x86_64.rpm ../RPMS/x86_64/frama-c-devel-1.4-4.fc12.x86_64.rpm 
frama-c.src: W: invalid-license QPL with modifications
frama-c.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: no-documentation
3 packages and 1 specfiles checked; 0 errors, 4 warnings.

The new warning is caused by removed duplicate documentation.  Since all documentation was duplicated it causes the documentation section for the devel RPM to become empty.  Its there but included in the base RPM.

I am starting a KOJI build now if it completes it is ready for a final review.

Comment 34 Mark Rader 2010-07-05 16:48:49 UTC
I completed the koji build and all built successfully under FC-14.

Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2296280
None
Watching tasks (this may be safely interrupted)...
2296280 build (dist-f14, frama-c-1.4-4.fc12.src.rpm): free
2296280 build (dist-f14, frama-c-1.4-4.fc12.src.rpm): free -> open (xb-01.phx2.fedoraproject.org)
  2296282 buildArch (frama-c-1.4-4.fc12.src.rpm, i686): free
  2296281 buildArch (frama-c-1.4-4.fc12.src.rpm, x86_64): open (xb-01.phx2.fedoraproject.org)
  2296282 buildArch (frama-c-1.4-4.fc12.src.rpm, i686): free -> open (x86-09.phx2.fedoraproject.org)
  2296282 buildArch (frama-c-1.4-4.fc12.src.rpm, i686): open (x86-09.phx2.fedoraproject.org) -> closed
  0 free  2 open  1 done  0 failed
  2296281 buildArch (frama-c-1.4-4.fc12.src.rpm, x86_64): open (xb-01.phx2.fedoraproject.org) -> closed
  0 free  1 open  2 done  0 failed
2296280 build (dist-f14, frama-c-1.4-4.fc12.src.rpm): open (xb-01.phx2.fedoraproject.org) -> closed
  0 free  0 open  3 done  0 failed

2296280 build (dist-f14, frama-c-1.4-4.fc12.src.rpm) completed successfully

Comment 35 David A. Wheeler 2010-07-16 21:49:31 UTC
Okay, I've started reviewing.  This new package builds on my system, and the only rpmlint messages were the ones noted above.

Comment 19 noted a number of "to-do" items, so I'm going to first go through all of the ones that had problems before:

* "I don't understand why this package installs "/usr/bin/ptests.byte"."

That's now gone, good.

* "Excluding the ".byte" files is fine.  But that means that this package won't
work on some architectures, so you need some ExcludeArch statements."

It now has an ExcludeArch statement, and I notice that you did a Koji test (that should tell you of problems like this).

* "I *still* don't understand this comment..."
  "The configure file uses graph.cmo in compiling a test program to
  check for ocamlgraph, but Fedora doesn't include this file in its
  distributions."

 I'm sorry, the comment changed, but new comment somehow got messed
 up and I *still* don't understand it.  It now says:
# The configure file uses graph.cmo in compiling a test program to
# check for ocamlgraph, but Fedora doesn't include this file in itshas changed the
# extension in later distributions to graph.cma .

  But "rpmls ocaml-ocamlgraph" shows:
-rw-r--r--  /usr/lib/ocaml/ocamlgraph/graph.cma
-rw-r--r--  /usr/lib/ocaml/ocamlgraph/graph.cmi
-rw-r--r--  /usr/lib/ocaml/ocamlgraph/graph.cmo

  The Fedora package *does* include the ".cmo" *and ".cma" file.
  I still don't understand what this spec is trying to say.
  (I realize that you inherited this package from others, so this is probably
  inherited as well, but it sure isn't clear as it is.)

* "I really think you should prefix the filename of Patch1 with "frama-c-"."

  Fixed, thanks!!

* "Patch2 (ptests) has *no* explanation, and that is NOT okay."

  All patches now have an explanation, good!

* "Nit: "plug in's" is still not a word."

  Using "plug ins" is not my preference, but I understand that you're
  trying to keep the spellchecker happy, so fine.

* "No %check section.  It's not required..."

  Still no %check section, but since it's not required... it's not required :-).

* "I'll check the %files list separately."

  Which I still need to do.

* "You really need to do a Koji build (see comment #18)...."

  Which you did, see comment 34. Thanks.

*  "MUST: rpmlint must be run on every package. The output should be posted
in the review.[1]"

  OK.

* MUST: The package must be licensed with a Fedora approved license and
meet the Licensing Guidelines .

OK, see comment 32.  I don't know why legal hasn't responded yet,
they really should.  But they approved the QPL, and the only
changes cannot affect its Freeness (see comment 32).
I'd like to hear anyone else's comments about this.

* MUST: The License field in the package spec file must match the actual
license. [3]

OK.

* MUST: If (and only if) the source package includes the text of the
license(s) in its own file, then that file, containing the text of the
license(s) for the package must be included in %doc.[4]

OK.  I checked the binary package with rpmls, and they're there.

* MUST: The package MUST successfully compile and build into binary rpms on
at least one primary architecture. [7]

OK.  I just did it, "works for me".

* MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in
bugzilla, describing the reason that the package does not compile/build/work on
that architecture. The bug number MUST be placed in a comment, next to the
corresponding ExcludeArch line. [8]

OK.  Added ExcludeArch, tested with Koji.

* MUST: All build dependencies must be listed in BuildRequires, except for
any that are listed in the exceptions section of the Packaging Guidelines ;
inclusion of those as BuildRequires is optional. Apply common sense.

OK.  Worked with Koji.

* MUST: Packages must NOT bundle copies of system libraries.[11]

OK.  As noted in earlier comments, this has a forked version of cil;
I don't see any way around this :-(, and you have
a reasonable justification in the spec comments.

* MUST: A Fedora package must not list a file more than once in the spec
file's %files listings. [14]

OK.  I didn't find any dups this time.

* MUST: If a package includes something as %doc, it must not affect the
runtime of the application. To summarize: If it is in %doc, the program must
run properly if it is not present. [18]

OK.  We now have some files marked as documentation.

* MUST: Header files must be in a -devel package. [19]

OK.

* MUST: Packages containing GUI applications must include a %{name}.desktop
file, and that file must be properly installed with desktop-file-install in the
%install section. If you feel that your packaged GUI application does not need
a .desktop file, you must put a comment in the spec file with your explanation.
[22]

OK, we now have a .desktop file.

This is looking really good.  I want to test it out, and do a clean read-through.  But other than my complaint about a comment (which I *still* don't understand) it's looking great so far.

Comment 36 David A. Wheeler 2010-07-16 22:01:27 UTC
Hmm, the SELinux configuration isn't working on Frama-C with Fedora 13, 32-bit.

When I select Applications/Programming/Frama-C, I get an SELinux alert. A copy-and-paste of the message is as follows:

Summary:

SELinux is preventing /usr/bin/frama-c-gui "execmod" access to
/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs.

Detailed Description:

SELinux denied access requested by frama-c-gui.
/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs may be a mislabeled.
/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs default SELinux type is
textrel_shlib_t, but its current type is lib_t. Changing this file back to the
default type, may fix your problem.

File contexts can be assigned to a file in the following ways.

  * Files created in a directory receive the file context of the parent
    directory by default.
  * The SELinux policy might override the default label inherited from the
    parent directory by specifying a process running in context A which creates
    a file in a directory labeled B will instead create the file with label C.
    An example of this would be the dhcp client running with the dhclient_t type
    and creating a file in the directory /etc. This file would normally receive
    the etc_t type due to parental inheritance but instead the file is labeled
    with the net_conf_t type because the SELinux policy specifies this.
  * Users can change the file context on a file using tools such as chcon, or
    restorecon.

This file could have been mislabeled either by user error, or if an normally
confined application was run under the wrong domain.

However, this might also indicate a bug in SELinux because the file should not
have been labeled with this type.

If you believe this is a bug, please file a bug report against this package.

Allowing Access:

You can restore the default system context to this file by executing the
restorecon command. restorecon '/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs', if
this file is a directory, you can recursively restore using restorecon -R
'/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs'.

Fix Command:

/sbin/restorecon '/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs'

Additional Information:

Source Context                unconfined_u:unconfined_r:unconfined_t:s0-s0:c0.c1
                              023
Target Context                system_u:object_r:lib_t:s0
Target Objects                /usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs [ file ]
Source                        frama-c
Source Path                   /usr/bin/frama-c
Port                          <Unknown>
Host                          fedora-devel
Source RPM Packages           frama-c-1.4-4.fc13
Target RPM Packages           frama-c-1.4-4.fc13
Policy RPM                    selinux-policy-3.7.19-33.fc13
Selinux Enabled               True
Policy Type                   targeted
Enforcing Mode                Enforcing
Plugin Name                   restorecon
Host Name                     fedora-devel
Platform                      Linux fedora-devel 2.6.33.5-124.fc13.i686 #1 SMP
                              Fri Jun 11 09:48:40 UTC 2010 i686 i686
Alert Count                   3
First Seen                    Fri 16 Jul 2010 05:53:13 PM EDT
Last Seen                     Fri 16 Jul 2010 05:58:59 PM EDT
Local ID                      60bb61f8-e4a2-45f5-8f6d-4623722057c4
Line Numbers                  

Raw Audit Messages            

node=fedora-devel type=AVC msg=audit(1279317539.414:36): avc:  denied  { execmod } for  pid=9573 comm="frama-c-gui" path="/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs" dev=dm-0 ino=440021 scontext=unconfined_u:unconfined_r:unconfined_t:s0-s0:c0.c1023 tcontext=system_u:object_r:lib_t:s0 tclass=file

node=fedora-devel type=SYSCALL msg=audit(1279317539.414:36): arch=40000003 syscall=125 success=no exit=-13 a0=6f3000 a1=5c000 a2=5 a3=bfa4d330 items=0 ppid=1 pid=9573 auid=500 uid=500 gid=500 euid=500 suid=500 fsuid=500 egid=500 sgid=500 fsgid=500 tty=(none) ses=1 comm="frama-c-gui" exe="/usr/bin/frama-c-gui" subj=unconfined_u:unconfined_r:unconfined_t:s0-s0:c0.c1023 key=(null)




Of course, the *BIG* thing is that we need for Frama-C and Why to talk to each other, so that we can use the -jessie option of Frama-C.

Comment 37 Richard W.M. Jones 2010-07-16 22:15:15 UTC
I believe the way to resolve this is to duplicate this bug
against selinux-policy component and ask them to write
and include a policy.

This should be done, but waiting for the policy doesn't
need to hold up the review.

Comment 38 Mark Rader 2010-07-18 15:47:28 UTC
Spec URL: http://tpath3.dnsalias.net/openproofs/frama-c.spec
SRPM URL: http://tpath3.dnsalias.net/openproofs/frama-c-1.4-5.fc12.src.rpm
Description:Frama-C is a suite of tools dedicated to the analysis of the
source code of software written in C.

I think I have corrected the SELinux error.  I have tested it on two systems multiple times deleting the SELinux entry each time.


[rader@tpath3 SPECS]$ rpmlint frama-c.spec ../SRPMS/frama-c-1.4-4.fc12.src.rpm ../RPMS/x86_64/frama-c-1.4-5.fc12.x86_64.rpm ../RPMS/x86_64/frama-c-devel-1.4-5.fc12.x86_64.rpm 
frama-c.src: W: invalid-license QPL with modifications
frama-c.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: no-documentation
3 packages and 1 specfiles checked; 0 errors, 4 warnings.

[rader@tpath3 SPECS]$ koji build --scratch dist-f14 ../SRPMS/frama-c-1.4-5.fc12.src.rpm 
Uploading srpm: ../SRPMS/frama-c-1.4-5.fc12.src.rpm
[====================================] 100% 00:01:32  18.84 MiB 207.62 KiB/sec
Created task: 2327526
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2327526
None
Watching tasks (this may be safely interrupted)...
2327526 build (dist-f14, frama-c-1.4-5.fc12.src.rpm): free
2327526 build (dist-f14, frama-c-1.4-5.fc12.src.rpm): free -> open (x86-12.phx2.fedoraproject.org)
  2327528 buildArch (frama-c-1.4-5.fc12.src.rpm, i686): free
  2327527 buildArch (frama-c-1.4-5.fc12.src.rpm, x86_64): free
  2327527 buildArch (frama-c-1.4-5.fc12.src.rpm, x86_64): free -> open (x86-20.phx2.fedoraproject.org)
  2327528 buildArch (frama-c-1.4-5.fc12.src.rpm, i686): free -> open (x86-18.phx2.fedoraproject.org)
  2327528 buildArch (frama-c-1.4-5.fc12.src.rpm, i686): open (x86-18.phx2.fedoraproject.org) -> closed
  0 free  2 open  1 done  0 failed
  2327527 buildArch (frama-c-1.4-5.fc12.src.rpm, x86_64): open (x86-20.phx2.fedoraproject.org) -> closed
  0 free  1 open  2 done  0 failed
2327526 build (dist-f14, frama-c-1.4-5.fc12.src.rpm): open (x86-12.phx2.fedoraproject.org) -> closed
  0 free  0 open  3 done  0 failed

2327526 build (dist-f14, frama-c-1.4-5.fc12.src.rpm) completed successfully

Comment 39 David A. Wheeler 2010-07-18 17:34:02 UTC
EXCELLENT.   This is looking awesome.

The SELinux fix works perfectly; at least for trivial uses, SELinux is now happy.  The new comment seems clear enough, too.

I should go back and see if the changes have messed up anything, or if there are big problems I didn't notice before, but so far it's looking great.

This version of Frama-C is not the current version.  If it'd be trivial to upgrade it to the current version, I think the *current* version would be best.  But if that's non-trivial, this version is a great place to start.  Would that upgrade be trivial, or not?

Comment 40 David A. Wheeler 2010-07-18 21:57:49 UTC
Okay, I understand that switching to the current version of Frama-C would be a big deal, due to dependencies on other packages.  So, let's go with the version of Frama-C that's packaged here.

All of the issues I identified earlier have been resolved, and I don't see any new issues to deal with.  So, thanks for your hard work!

APPROVED.

Comment 41 Mark Rader 2010-07-19 02:23:23 UTC
David

Per your comment, "This version of Frama-C is not the current version.  If it'd be trivial to
upgrade it to the current version, I think the *current* version would be best.
 But if that's non-trivial, this version is a great place to start.  Would that
upgrade be trivial, or not?"  It is definitely non trivial.  Let me explain so that we can document.  

I tried to perform a substitution for the package just as a sanity check.  It error'ed on the strip of frama-c and frama-c-gui.  On checking these had not built.  I thne tried to do a manual build and no jou.  They still did not build.  I next tried to force a build and got the following confiuration error.

 checking for /usr/lib64/ocaml/dynlink.cmxa... yes
checking for lablgtk2's custom tree model... yes
configure: *************************************
configure: * CHECKING FOR PLUG-IN DEPENDENCIES *
configure: *************************************
configure: WARNING: ltl2ba not found.
configure: WARNING: aorai partially enabled because ltl2ba missing.
configure: WARNING: lablgtksourceview2.cmxa not found
configure: error: gui requested but /usr/lib64/ocaml/lablgtk2/lablgtksourceview2.cmxa missing.


The missing file is part of OCAML.  Particularly it is part of LABLGTK, however it is part of lablgtk2 which has not been packaged so we will need to request it be packaged, package it ourselves or find some solution.  I dont know what else may be missing but the newer version is looking at some effort.

Comment 42 Richard W.M. Jones 2010-07-19 10:23:16 UTC
(In reply to comment #41)
> configure: error: gui requested but
> /usr/lib64/ocaml/lablgtk2/lablgtksourceview2.cmxa missing.
> 
> 
> The missing file is part of OCAML.  Particularly it is part of LABLGTK, however
> it is part of lablgtk2 which has not been packaged so we will need to request
> it be packaged, package it ourselves or find some solution.  I dont know what
> else may be missing but the newer version is looking at some effort.    

Is this a regression of bug 462651 I wonder?

Comment 43 Mark Rader 2010-07-19 12:47:33 UTC
It is possible however that but had issues with lablgtksourceview.cma not lablgtksourceview2.cmxa.  I just know that I can not find the lablgtk2 package in the standard yum repositories.  It may be in the rawhide repository and my system is not configured for it.  This just complicates matters and adds considerable time.

Comment 44 Richard W.M. Jones 2010-07-19 13:02:07 UTC
(In reply to comment #43)
> It is possible however that but had issues with lablgtksourceview.cma not
> lablgtksourceview2.cmxa.  I just know that I can not find the lablgtk2 package
> in the standard yum repositories.  It may be in the rawhide repository and my
> system is not configured for it.  This just complicates matters and adds
> considerable time.    

Not sure what you mean by can't find it.  ocaml-lablgtk is
in Fedora for ages (years).

Comment 45 Mark Rader 2010-07-20 23:46:07 UTC
New Package CVS Request
=======================
Package Name: frama-c
Short Description: mathematical code validation interface
Owners: mrader
Branches: F-12 F-13 F-14
InitialCC: mrader

Comment 46 Kevin Fenzi 2010-07-21 05:15:11 UTC
CVS done (by process-cvs-requests.py).

We are not currently doing F-14 branches yet. Otherwise done.

Comment 47 Chen Lei 2010-07-28 12:51:46 UTC
Some suggestions:

1. Why not package the latest version - frama-c-Boron-20100401 instead? 

2.I think Development/Libraries should be changed to Development/Tools.

3.
%{_datadir}/applications should not be listed in %file, you need to use %{_datadir}/applications/*.desktop instead.

4.
I suggest to rename %{name}.desktop to %{name}-gui.desktop. Actually, frama-c is a command line tool.

5.
ExcludeArch: PPC, PPC64, ARM, IA64, MIPS, S390

I think you should use ExclusiveArch:  alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9 ppc64 instead to keep consistency with ocaml.

Comment 48 David A. Wheeler 2010-07-28 14:05:08 UTC
Comment 47 has some good points.

Regarding: "1. Why not package the latest version - frama-c-Boron-20100401 instead?"  I'd really like to see that happen, but there are reasons that the current one isn't packaged yet.  In particular, ocaml-lablgtk needs to get updated (feel free to badger Richard W.M. Jones :-) ).  Details below.

First, I completely agree that it'd be *great* to update frama-c to the current version.  I have an updated packaging of "why" that *cannot* be used until the latest version of frama-c is packaged, so I would ALSO like to see the latest version of frama-c (Boron-20100401) packaged.

I asked the Fedora frama-c packager (Mark Rader) to explain why he didn't package the latest version.  He explained to me that at least one problem is that the latest version of frama-c requires gtksourceview2, but the ocaml-lablgtk package in Fedora does *NOT* include support for gtksourceview2 (it only supports gtksourceview 1.0).   This is a fundamental blocker to updating to the current version of Frama-C.

I've already sent a patch to Richard W.M. Jones to modify ocaml-lablgtk so that it adds support for gtksourceview2.  (I sent it yesterday, before I saw your email, so great minds think alike I guess).  It's a trivial patch, so I really hope it will be added ASAP.  It forces a lot of rebuilds of other OCaml packages, but that's a one-time event and I think it *should* be done.

The best instructions I know of for Fedora are (and it's painful): http://itrs.tw/wiki/Frama-C_Installation_Note_on_Fedora_12

There may be other issues.  I know that for best results ltl2ba needs to be packaged, and there may be issues with ocamlgraph too.  If you could help, that'd be GREAT!!!!

For completeness, here's my patch to the spec file of ocaml-lablgtk as it exists in Fedora 13:

 Name:           ocaml-lablgtk
 Version:        2.14.0
-Release:        4%{?dist}
+Release:        5%{?dist}
 
 Summary:        Objective Caml interface to gtk+
 
@@ -34,6 +34,7 @@
 BuildRequires:  ocaml-ocamldoc
 BuildRequires:  zlib-devel
 BuildRequires:  gtksourceview-devel
+BuildRequires:  gtksourceview2-devel
 
 
 %global __ocaml_requires_opts -i GtkSourceView_types -i GtkSourceView2_types
@@ -79,6 +80,7 @@
 %configure --with-gl --enable-debug
 perl -pi -e "s|-O|$RPM_OPT_FLAGS|" src/Makefile
 make world
+make opt
 make doc CAMLP4O="camlp4o -I %{_libdir}/ocaml/camlp4/Camlp4Parsers"
 
 
@@ -152,6 +154,9 @@
 
 
 %changelog
+* Tue Jul 27 2010 David A. Wheeler <dwheeler> - 2.14.0-5
+- Add support for gtksourceview2 (in addition to gtksourceview 1.0).
+
 * Tue Jan  5 2010 Richard W.M. Jones <rjones> - 2.14.0-4
 - Use upstream RPM 4.8 dependency generator.
 - -devel package should depend on gtk2-devel, otherwise lablgtk programs

Comment 49 Mark Rader 2010-07-28 14:36:03 UTC
1.  I tend to agree with you on the frama-c-Boron vs the older version but as David noted the technical difficulties became greater than a simple switch and sometimes it is better to get it out there than just keep trying to get the latest and greatest.

2.  Since this has been put in the repository and is now available as a package, I will see about changing this for the next version.

3.  Since this has been put in the repository and is now available as a package, I will see about changing this for the next version.

4.  Since this has been put in the repository and is now available as a package, I will see about changing this for the next version.  Actually frama-c has both.  you have frama-c (command line) and frama-c-gui which is the gui.  

5.  Not as familiar with that command.  I will look into it.


(In reply to comment #47)
> Some suggestions:
> 
> 1. Why not package the latest version - frama-c-Boron-20100401 instead? 
> 
> 2.I think Development/Libraries should be changed to Development/Tools.
> 
> 3.
> %{_datadir}/applications should not be listed in %file, you need to use
> %{_datadir}/applications/*.desktop instead.
> 
> 4.
> I suggest to rename %{name}.desktop to %{name}-gui.desktop. Actually, frama-c
> is a command line tool.
> 
> 5.
> ExcludeArch: PPC, PPC64, ARM, IA64, MIPS, S390
> 
> I think you should use ExclusiveArch:  alpha armv4l %{ix86} ia64 x86_64 ppc
> sparc sparcv9 ppc64 instead to keep consistency with ocaml.

Comment 50 David A. Wheeler 2010-07-29 20:12:26 UTC
An update on Comment 48:

Richard Jones has permitted me to become a co-maintainer of ocaml-lablgtk.  I intend to modify its spec file for at least Fedora 13 and 14 to add support for gtksourceview2.  That is a necessary step to package the latest version of Frama.C-.

We'll have to wait til the Fedora 14 branching is complete; hopefully that won't be too long.

Comment 51 Mark Rader 2010-08-01 13:59:08 UTC
All

I corrected the following.

%{_datadir}/applications should not be listed in %file, you need to use
%{_datadir}/applications/*.desktop instead.

Mark Rader

Comment 52 David A. Wheeler 2010-08-01 17:55:17 UTC
A few notes regarding Frama-C:

1. Frama-C can optionally use ltl2ba, which adds some functionality.
I have packaged ltl2ba, review request here:
 https://bugzilla.redhat.com/show_bug.cgi?id=619831

2. I have updated ocaml-lablgtk in Fedora 13 so that it supports for gtksourceview2.  This is required for the latest (unpackaged) version of Frama-C.   Please test and vote for it, by seeing:
https://admin.fedoraproject.org/updates/ocaml-lablgtk-2.14.0-5.fc13

3. I tried to also update ocaml-lablgtk to support gtksourceview2 on Fedora 14.  Unfortunately, the build mysteriously failed.  When it tried to compile 'ml_gobject.c' it reported the error "ml_gobject.c:292:14: error: conflicting types for 'g_value_get_variant'".

My *hope* is that this failed build was caused by some of the problems due to the infrastructure transition we're undergoing, and that the problem will go away soon.  You can see the task results here (see the failed build's build.log for details):
http://koji.fedoraproject.org/koji/taskinfo?taskID=2369292

Unfortunately, I think that is *not* the case.  It appears that newer versions of the ocaml compiler have made a change that breaks many programs, including lablgtk.  The ocaml compiler change is noted here: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
Here's the info regarding lablgtk specifically:
http://permalink.gmane.org/gmane.comp.lang.ocaml.lib.gtk/1491

The recommended solution seems to be to compile/package a snapshot from here:
 http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
Suggestions welcome.

Comment 53 Richard W.M. Jones 2012-08-01 09:58:38 UTC
frama-c has been in Fedora for quite a long time.


Note You need to log in before you can comment on or make changes to this bug.