Thanks for creating this package!!  I know this was rough to package.  I'll post comments later.

*** Bug 448502 has been marked as a duplicate of this bug. ***

It didn't build for me on Fedora 12 x86_64, with error:
  /usr/bin/ld: cannot find -lgtksourceview-1.0
You need to add this to the spec:
 BuildRequires: gtksourceview-devel

Here are some initial comments from reading the .spec file:

* Thanks for working out the complicated licensing situation.
  Hopefully Fedora legal will reply soon re: QPL with modifications.

* I suggest emailing Medhi Dogguy re: the Debian patches, and then
  changing the comments to document with certainty the decisions. E.G.:
  # This seems to apply for us as well, keeping Debian filename
  should be (once you've confirmed):
  # This applies to us as well...

  # I don't know why we would want to use that Jessie -> not including this patch
  should be:
   # We won't embed Jessie, but will instead use the Jessie supplied by the Why package

  # I'm not sure quite what this patch does, but I'm going to leave it out for now
  :-).

  # I didn't see any Fedora package providing the files that this patch
  # references -> dropping for now
  I don't have the patch you dropped, but it's worth noting that Fedora 12 provides
  packages named gtksourceview *and* gtksourceview2, as well as their -devel packages.
  Are these what you're looking for?

  In general, I know that people prefer relatively few lines in .spec files.

* You need to rename this source (patch) file:
   0001-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch
   First, the ".." should be ".", and the prefix should be %{name}-%{version}-
   so that multiple simultaneous builds in the same SOURCE directory
   won't cause trouble.

* You should have a brief "why you need this" comment above:
  %if 0%{?fedora} >= 13
  Patch2: frama-c-1.4-ptests-fix-for-ocaml-3.11.2.patch 
  %endif

* As I noted earlier, you need gtksourceview-devel as a BuildRequires,
  or the build may fail.

* You use a macro here inside a comment, which will trigger a warning:
  # %check
  # make ptests %{frama-c_make_options}
  # make oracles %{frama-c_make_options}

  I suggest using "with" to make these disabled by default, but enable-able. E.G.:
  %if %{with lengthy-tests}
  %check
  make ptests %{frama-c_make_options}
  make oracles %{frama-c_make_options}
  %endif

  It'd be even better if you had at least a few tests run even without enabling "lengthy-tests",
  but this would at least make it easy to enable the lengthy test and would eliminate rpmlint complaints.

* The package includes over 20M of documentation; I think the documentation
   should be in a separate subpackage.

* It starts with "# Some ideas for this spec file taken from a prior attempt by Richard W. M. Jones"
  I think it's great to give credit, but you might consider moving that to the bottom as part of the comments
  in the ChangeLog.  Not a requirement.

Regarding the upstream version naming convention... I agree with you, the upstream naming convention is awful (e.g., "Beryllium").  This is an odd duck, and I'd like to hear others' comments.

I looked over the Fedora policy, here, on version numbers:
http://fedoraproject.org/wiki/Packaging/NamingGuidelines#Package_Version
The policy focuses on the situations where non-numeric version identifiers are Pre-release packages (e.g., "alpha"), Post-release packages (e.g., "1.3a"), snapshots, and Jpackage-derived packages.  None of these situations applies.  In this case, we have a group that gives alphabetic names to versions, and you'd have to know the periodic table to know which is newer.

We *could* use a YYYYMMDD system, but that is a little awkward.

Translating the element names into their numeric atomic number (number of protons) isn't a bad idea at all, but I think you should use "0." as the prefix instead of "1.".  This means that Beryllium would become "0.4".  That way, if they switch to a more conventional version numbering system in the future, we can switch to it without using epochs.  In addition, I think you should add the word "beryllium" to the release name, so that people can easily figure out which one they have.

I'd be curious to hear others' thoughts on version/release naming.

Agreed re comment 5.

Note: The latest version of Frama-C is actually "Beryllium 2".  If we switch to using numeric version numbering beginning with "0.", then I think "Beryllium 2" should translate to version number "0.4.2".

Note: Fedora packages Why version 2.23, not Why version 2.21.
That's not a problem, in fact, that's a GOOD thing
(Why version 2.23 has many more capabilities).
However, it means that the Frama-C documentation for
Jessie does NOT work as-is, because they changed a default setting in
Why's Jessie.

So, what's changed?
As of Why version 2.22, Jessie now requires proof of
termination by default.  This is a good change, because the previous
semantics were tripping people up.  The newer versions of Why also
have FAR better support for termination proofs (since they made it the
default, they suddenly had to support it better :-) ).
However, since it no longer works as-is with the included docs, there
should be SOMETHING in the package that documents this change.

So I recommend including a file with the following content, or something
like it, as a %doc.   Call it "frama-c-1.4.why-changes.txt" or
something like it:

============================================================
Note that when Frama-C is used with Why version 2.22 or greater, there
is an important change in the semantics of Jessie.

In Why version 2.21's Jessie component, by default you did NOT need
to prove termination.  This resulted in some surprises and problems for users.
Thus, starting in Why version 2.22, Jessie requires proof of
termination by default.

As a result, many of the examples in the Frama-C Beryllium documentation
for Jessie do not work as-is, because they
don't include termination information.  For more information, see:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001736.html

For example, the Jessie tutorial section 2.2 needs to have a "loop variant"
added.  What's more, this MUST be added using
the /*@...*/ form NOT the //@ forms (you can't have adjacent //@ forms).
Here is what the updated example in section 2.2 looks like:

/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */

//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1, p = -1;
  /*@ loop invariant 0 <= l && u <= n-1;
    @ loop variant u-l; */
  while (l <= u ) {
    int m = l + (u - l) / 2; // NOTE this is changed for bounded calculation
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else {
      p = m; break;
    }
  }
  return p;
}

I've started to walk through the Fedora Guidelines and comparing with this draft package.  Here are some more comments.

The %files list isn't right.  It ends with:
 %exclude %{_datadir}/frama-c
which makes these lines pointless:
 %{_datadir}/frama-c/why
 %{_datadir}/frama-c/manuals
Basically, %{_datadir}/frama-c/why and ../manuals don't get packaged at all.
The file list in -devel don't look right at all to me; they look like examples
but NOT code necessary for developers depending on frama-c.
(See http://fedoraproject.org/wiki/Packaging:OCaml for more on OCaml -devel packages.)
I suggest re-examining the %files list, so that they get split more cleanly
*AND* so that there's a -doc subpackage.

Strictly speaking, what you're packaging is "Frama-C Beryllium 2" not "Beryllium".

This package contains a GUI, so there should be a .desktop file.

The Makefile uses "$(CP)" everywhere, but its definition (in share/Makefile.common) doesn't preserve timestamps (this impacts the 'make install' in the -devel package in particular).  You need to try to preserve timestamps.  One way would be to modify share/Makefile.common so that:
 CP      = cp -f
becomes:
 CP      = cp -f --preserve=timestamps


Have you tried passing the SMP flags, e.g.:
  make %{?_smp_mflags}
if that FAILS, then that should be documented, otherwise you should try to build using SMP.


Thanks for working on this package, I really appreciate it.

(In reply to comment #5)
> Regarding the upstream version naming convention... I agree with you, the
> upstream naming convention is awful (e.g., "Beryllium").  This is an odd duck,
> and I'd like to hear others' comments.
> 
> I looked over the Fedora policy, here, on version numbers:
> http://fedoraproject.org/wiki/Packaging/NamingGuidelines#Package_Version
> The policy focuses on the situations where non-numeric version identifiers are
> Pre-release packages (e.g., "alpha"), Post-release packages (e.g., "1.3a"),
> snapshots, and Jpackage-derived packages.  None of these situations applies. 
> In this case, we have a group that gives alphabetic names to versions, and
> you'd have to know the periodic table to know which is newer.
> 
> We *could* use a YYYYMMDD system, but that is a little awkward.
> 
> Translating the element names into their numeric atomic number (number of
> protons) isn't a bad idea at all, but I think you should use "0." as the prefix
> instead of "1.".  This means that Beryllium would become "0.4".  That way, if
> they switch to a more conventional version numbering system in the future, we
> can switch to it without using epochs.  In addition, I think you should add the
> word "beryllium" to the release name, so that people can easily figure out
> which one they have.
> 
> I'd be curious to hear others' thoughts on version/release naming.    

So, to clarify, you're suggesting a release of something like "2.beryllium"? (The other way around would affect EVR comparisons, no?)

(In reply to comment #9)
> I've started to walk through the Fedora Guidelines and comparing with this
> draft package.  Here are some more comments.
> 
> The %files list isn't right.  It ends with:
>  %exclude %{_datadir}/frama-c

That is a mistake on my part.

> which makes these lines pointless:
>  %{_datadir}/frama-c/why
>  %{_datadir}/frama-c/manuals
> Basically, %{_datadir}/frama-c/why and ../manuals don't get packaged at all.
> The file list in -devel don't look right at all to me; they look like examples
> but NOT code necessary for developers depending on frama-c.
> (See http://fedoraproject.org/wiki/Packaging:OCaml for more on OCaml -devel
> packages.)
> I suggest re-examining the %files list, so that they get split more cleanly
> *AND* so that there's a -doc subpackage.

What I wanted to put in there was the code that is necessary to compile plugins with Frama-C. At minimum, the Makefiles in that group are necessary, and I thought that the extra files in there were necessary for plugin compilation, but this appears to be untrue - I will need to re-examine exactly what is necessary for plugin compilation. (It may well be more of the files as in a conventional OCaml package, but to begin with I purposely did not package this like an OCaml library because I thought one would not need some of the Frama-C files.)

I suppose the documentation is large enough to require a doc package.

> Strictly speaking, what you're packaging is "Frama-C Beryllium 2" not
> "Beryllium".

True.

> This package contains a GUI, so there should be a .desktop file.

Also true.

> The Makefile uses "$(CP)" everywhere, but its definition (in
> share/Makefile.common) doesn't preserve timestamps (this impacts the 'make
> install' in the -devel package in particular).  You need to try to preserve
> timestamps.  One way would be to modify share/Makefile.common so that:
>  CP      = cp -f
> becomes:
>  CP      = cp -f --preserve=timestamps
>
> Have you tried passing the SMP flags, e.g.:
>   make %{?_smp_mflags}
> if that FAILS, then that should be documented, otherwise you should try to
> build using SMP.

I'll make these last two changes as well.

(In reply to comment #10)

The basic question is how to convert the version name "Beryllium 2" into something reasonable.  Sorry to have such a long conversation about version/release id's, but upstream's version naming convention is hideous and it's not directly covered by the Fedora guidelines.  Anyway, I looked at this for some guidance:
http://fedoraproject.org/wiki/Packaging/NamingGuidelines#Package_Version

Since Beryllium has atomic number 4, this is subrelease 2 of the Beryllium version, and we should prefix with "0." (see comment #5 and comment #6), then I think we should have:
 Version: 0.4.2

We could have a perfectly reasonable 'release' value like this, since 0.4.2 would uniquely map to Beryllium 2:
 Release: 1%{?dist}
Having a simple 'release' value has its own virtues, and that'd be quite reasonable.

However, what I was thinking was that many people might not understand that version "0.4.2" was the same thing as "Beryllium 2" (unless they look up our translation gimmick).   The "Release" value is where nonnumeric version id's hide, so I was thinking that we might use the Release field to provide that info to users.  E.G., perhaps something like this for Beryllium 2:
 Release: 1.beryllium.2%{?dist}

Then the initial release number would be incremented for each new package release of Beryllium 2.

Does that sound reasonable?  Comments, anyone?

(In reply to comment #12)
> (In reply to comment #10)
> 
> The basic question is how to convert the version name "Beryllium 2" into
> something reasonable.  Sorry to have such a long conversation about
> version/release id's, but upstream's version naming convention is hideous and
> it's not directly covered by the Fedora guidelines.  Anyway, I looked at this
> for some guidance:
> http://fedoraproject.org/wiki/Packaging/NamingGuidelines#Package_Version
> 
> Since Beryllium has atomic number 4, this is subrelease 2 of the Beryllium
> version, and we should prefix with "0." (see comment #5 and comment #6), then I
> think we should have:
>  Version: 0.4.2
> 
> We could have a perfectly reasonable 'release' value like this, since 0.4.2
> would uniquely map to Beryllium 2:
>  Release: 1%{?dist}
> Having a simple 'release' value has its own virtues, and that'd be quite
> reasonable.
> 
> However, what I was thinking was that many people might not understand that
> version "0.4.2" was the same thing as "Beryllium 2" (unless they look up our
> translation gimmick).   The "Release" value is where nonnumeric version id's
> hide, so I was thinking that we might use the Release field to provide that
> info to users.  E.G., perhaps something like this for Beryllium 2:
>  Release: 1.beryllium.2%{?dist}
> 
> Then the initial release number would be incremented for each new package
> release of Beryllium 2.
> 
> Does that sound reasonable?  Comments, anyone?    

Sounds fine to me. I've gone some of the distance toward making the revisions you wanted. New SRPM at

https://www.openproofs.org/packages/frama-c/frama-c-0.4.2-1.Beryllium.2.fc12.src.rpm

(spec file location is the same)

Changes made:
- Now has a doc subpackage, desktop file
- Version name changed
- cp timestamps modification
- Added short tests/long tests option (short tests is default unless "with lengthy_tests")
- Patch rename and justification as above
- Builds in Koji (http://koji.fedoraproject.org/koji/taskinfo?taskID=2004214) thanks to fixed BuildRequires

Still to do:
- Talk to Medhi Dogguy about functionality of some of the patches
- Get word from Fedora Legal
- SELinux issues
- Repackage -devel subpackage (exact contents necessary still unknown...)
- SMP flags

Congrats on making progress...!

> Still to do...
>- SELinux issues
>- Repackage -devel subpackage (exact contents necessary still unknown...)
>- SMP flags 

Do you need help on any of this?  If you do, what help do you need?

I will be taking over the package from Allan Dunn in the next week.  I will post it when the takeover is completed and I will submit it as a new bug report.

No need for a new bug, just post an update here.

Regarding the SELinux, that I understand to be related to dynamic loading in OCaml, Frama-C's only fault is to be the first packaged OCaml program that uses dynamic loading. If something can be done to have OCaml produce dynamically linkable code that satisfies SELinux, it should be done at the level of the compiler.
Assuming dynamic loading is the problem, the issue can be worked around with ./configure -with-all-static. But then there will be a monolithic executable, and that may not be the way you would like to package it.

I would also urge you NOT to invent a new numbering scheme for versions. "Boron", "Beryllium 2", etc... are nicknames with no numerical significance. The next release could be named "Steel". There is already a version number for the last release, and this number is 20100401. If you were looking for major and minor numbers indicating compatibility, please consider that every release is a new major release. There has never been a Frama-C release that was compatible with a previous version and the next one won't be either, trust me.

Well I got the package to build successfully and build the SRPMS, and RPMS.  I have used the rpmlint tool on all of the packages with the following result.

rpmlint frama-c.spec ../RPMS/x86_64/frama-c-1.4-1.fc12.x86_64.rpm ../RPMS/x86_64/frama-c-devel-1.4-1.fc12.x86_64.rpm ../SRPMS/frama-c-1.4-1.fc12.src.rpm

frama-c.spec:111: W: make-check-outside-check-section # make tests | grep --silent "Ok  = 1579 of 1581"

frama-c.x86_64: W: invalid-license QPL with modifications

frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c
frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c-gui
frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c.byte
frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c-gui.byte
frama-c.x86_64: W: unstripped-binary-or-object /usr/lib64/frama-c/plugins/Ltl_to_acsl.cmxs

frama-c-devel.x86_64: W: spelling-error %description -l en_US plugins -> plug ins, plug-ins, plugging

frama-c-devel.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: no-documentation

frama-c.src: W: invalid-license QPL with modifications
frama-c.src:111: W: make-check-outside-check-section # make tests | grep --silent "Ok  = 1579 of 1581"

The first warning should be easy to fix and that should also fix the last warning.  We need to check out the license issues so that should help.  Does anyone have an idea what the stripped-binary-or-object error is caused by and how to fix it, or is it even an issue.

I checked ou the invalid license issue.  The QPL license with modifications are included with the source.  The modifications are as follows:

"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."

So I don't see this as an issue.  QPL seems to generally be the same as GPL and this allows for the base use of the library that will not be publicly released.

Adding exceptions to a license is fine.  It allows people to do more things
(make the license more towards BSD).

Have you tried stripping the executables that rpmlint complains about?
Make sure they still run after they've been stripped though.

As an update:

I have fixed the following:
frama-c.spec:111: W: make-check-outside-check-section # make tests | grep
--silent "Ok  = 1579 of 1581"

From reading the license and the comment above:
frama-c-devel.x86_64: W: invalid-license QPL with modifications
This does not appear to be an issue.

This error:
frama-c-devel.x86_64: W: spelling-error %description -l en_US plugins -> plug
ins, plug-ins, plugging
appears to be minor and more of annoyance.  I can not find anything relating to this in the .spec file or in the source code.

As for the error unstripped-binary-or-object messages, I talked with David Wheeler and the problem may be with an inproper stripping rather than the binaries not being stripped.  I am not sure if this is actually necessary.

All

The latest rpmlint output is as follows:

rpmlint frama-c.spec ../RPMS/x86_64/frama-c-1.4-1.fc12.x86_64.rpm ../RPMS/x86_64/frama-c-devel-1.4-1.fc12.x86_64.rpm ../SRPMS/frama-c-1.4-1.fc12.src.rpm 

frama-c.x86_64: W: invalid-license QPL with modifications
frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c.byte
frama-c.x86_64: W: unstripped-binary-or-object /usr/bin/frama-c-gui.byte
frama-c.x86_64: W: unstripped-binary-or-object /usr/lib64/frama-c/plugins/Ltl_to_acsl.cmxs

frama-c-devel.x86_64: W: invalid-license QPL with modifications
frama-c-devel.x86_64: W: no-documentation

frama-c.src: W: invalid-license QPL with modifications

3 packages and 1 specfiles checked; 0 errors, 7 warnings

As stated before the QPL modifications do not seem to be an issue.  They just make the license less restrictive.  I have the code stripping two of the binaries but the unstripped binarys appear to be libraries especially the last one.  I will post the latest update to the package this weekend.

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
RPM URL:
http://tpath3.dnsalias.net/openproofs/frama-c-1.4-1.fc12.x86_64.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 also.

I updated the installation and now it adds the frama-c specific library to the selinux database.  So that I need to find out how, at installation time to require a helper package, graphviz-dev,  this is not required for compile only to run certain functions?  It is ready for someone to start examining.

(In reply to comment #24)
> It is ready for someone to start examining.    

This won't just happen by magic.  You need to negotiate with
someone to get them to do a review, perhaps involving swapping
one of their reviews for this one.  Ask about it on one of the Fedora
general development mailing lists.

(In reply to comment #25)
> (In reply to comment #24)
> > It is ready for someone to start examining.    
> 
> This won't just happen by magic.  You need to negotiate with
> someone to get them to do a review, perhaps involving swapping
> one of their reviews for this one.  Ask about it on one of the Fedora
> general development mailing lists.    

Which one would you recommend?

Fedora devel is the right place:
https://admin.fedoraproject.org/mailman/listinfo/devel

Here are some examples of people asking for review swaps which you
can use as a basis for your requests:

http://markmail.org/message/eg5bkc3dg4df3oag
http://lists.fedoraproject.org/pipermail/devel/2010-April/135369.html
http://lists.fedoraproject.org/pipermail/devel/2010-April/134527.html
http://lists.fedoraproject.org/pipermail/devel/2010-March/133783.html

I suggest you follow up to that email and offer to swap a review with
someone.  It's good as well because you'll get practice doing reviews.

I have created a new bug report so that I can edit settings and obtain sponsorship.  The new bug is:

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

*** This bug has been marked as a duplicate of bug 592579 ***