Bug 769958

Summary: Review Request: eqp - Automated theorem prover for first-order equational logic
Product: [Fedora] Fedora Reporter: John C Peterson <jcp>
Component: Package ReviewAssignee: Nobody's working on this, feel free to take it <nobody>
Status: NEW --- QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: unspecified    
Version: rawhideCC: james.hogarth, jcp, mario.blaettermann, package-review, robinlee.sysu, tcallawa
Target Milestone: ---   
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Attachments:
Description Flags
Patch to fix printf on 64-bit systems none

Description John C Peterson 2011-12-22 15:19:54 EST
Spec URL: http://www.eskimo.com/~jcp/eqp.spec
SRPM URL: http://www.eskimo.com/~jcp/eqp-09e-1.fc16.src.rpm
Description: EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search. It seems to perform well on many problems about lattice-like structures.

EQP is not a stable and polished production theorem prover like Otter or Prover9. Since it has obtained several interesting results, it was decided to make it available (including the source code) to everyone, with no restrictions (and of course no warranty either). EQP's documentation is not great, but if you already know Otter, you probably will not have great difficulty in learning to use EQP.
Comment 1 Jerry James 2011-12-22 18:39:17 EST
Created attachment 549255 [details]
Patch to fix printf on 64-bit systems

John, as discussed in email, I'll sponsor you.

I have a few minor preliminary comments, and one showstopper to bring up before doing a full review.  First the showstopper: the license.  The text you quote in eqp-09e-license.patch does NOT say that the authors are abandoning copyright, which is what a public domain declaration amounts to.  It merely says they want to make eqp available to everyone, which they have done by putting it on their web site.  For Fedora's purposes, we need to know that they are granting the rights to redistribute, and to modify.  That can probably be read into the "with no restrictions" clause, but I'm not comfortable making that judgment myself.  You need to either: (1) get the authors to clarify the rights they are granting, preferably with a standard license; or (2) write to fedora-legal-list@redhat.com and see if this statement counts as "Freely redistributable without restriction"; see https://fedoraproject.org/wiki/Packaging:LicensingGuidelines#.22Distributable.22.  I strongly encourage you to try (1) before (2).

Now for some minor stuff.

The first line of %install and the entire %clean script are not needed in Fedora; rpm automatically removes the build root in both cases.  Likewise, the %defattr in %files is now automatic in Fedora.  They are still needed for RHEL, though, so if you intend to share the spec file between the two distributions, then just leave it as is.  I'll note that I haven't seen the [ "$RPM_BUILD_ROOT" != "/" ] part for years; wow, that takes me back to the time when RPM_BUILD_ROOT *was* "/" and I trashed my system while trying to build an rpm.  I can laugh now, but it wasn't so funny then....  Anyway, rpm hasn't allowed RPM_BUILD_ROOT to be "/" for years, so that part is superfluous, even on RHEL.

The script examples/go pulls in /bin/csh as a dependency.  This is a no-no for documentation; see https://fedoraproject.org/wiki/Packaging:Guidelines#Documentation.  You either need to remove the executable bits from that script, drop the script from %doc altogether, or create a separate subpackage for the examples, with that script in %{_bindir} (suitably renamed, of course).

The patch to use long int on 64 bit systems is being applied whether the system is 64 bit or not.  On 32 bit systems, this leads to warnings like these:

unify.c: In function 'print_unify_mem':
unify.c:142:236: warning: format '%ld' expects argument of type 'long int', but argument 3 has type 'unsigned int' [-Wformat]

See the attached patch for an alternate approach that should work on both 32 and 64 bit systems.

Also, each patch needs a comment about its upstream status; see https://fedoraproject.org/wiki/Packaging:Guidelines#All_patches_should_have_an_upstream_bug_link_or_comment.

This is totally up to you, but you could eliminate eqp-09e-makefile.patch by invoking make like this:

make CFLAGS="$RPM_OPT_FLAGS -DTP_RUSAGE" eqp

and then installing like this:

install -m 755 eqp%{version} ${RPM_BUILD_ROOT}%{_bindir}/eqp

That would be one less patch to put an upstream status comment on.
Comment 2 John C Peterson 2011-12-23 16:34:20 EST
Spec URL: http://www.eskimo.com/~jcp/eqp.spec
SRPM URL: http://www.eskimo.com/~jcp/eqp-09e-2.fc16.src.rpm

Jerry - thanks again for sponsoring me.

I think I have fixed all of the minor issues you have raised.

As you suggested, I just eliminated the patch to the Makefile and made the corresponding adjustments to the make command in the %build section.

The "go" script in the examples sub-directory is rather trivial as you can see by inspection, so it really doesn't warrant an examples sub-package. I elected to just remove the executable permission bits. It could also be entirely eliminated from the package if that is in some way preferable.

I eliminated the checks in %install and %clean for RPM_BUILD_ROOT being equal to "/" as you suggested.  Just the thought of that happening is enough to make my hair stand on end, so I have included it in all my personal packages for ages now.  (I guess I am dating myself by including that :^)

Your patch for the printf statements is a much better solution than mine, and as you said, it also works independent of the host architecture.

The issues relating to the licensing are a valid concern of course, but could be a show stopper in this case because there is no upstream to contact regarding this issue (or the filing of bug reports). The author, William McCune, passed away rather suddenly back in May 2011. A shocker to the ATP community for sure as he was only 58!

http://www.cs.unm.edu/~veroff/ADAM/2011/

I will contact fedora-legal-list@redhat.com as you suggested. It's worth a try.

I doubt that it would be of any help in making a legal clarification, but Bill was also the author of Prover9/Mace which is already packaged in Fedora as prover9. That package is licensed under GPLv2 and GPLv2+, but the prover9 source distribution includes a file named COPYING that clearly states that, which is not the case for EQP.
Comment 3 Mario Bl├Ąttermann 2012-10-06 15:42:48 EDT
Scratch build:
http://koji.fedoraproject.org/koji/taskinfo?taskID=4567138

$ rpmlint -i -v *
eqp.src: I: checking
eqp.src: W: spelling-error Summary(en_US) prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.src: W: spelling-error Summary(en_US) equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.src: W: spelling-error %description -l en_US equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.src: W: spelling-error %description -l en_US prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.src: W: spelling-error %description -l en_US usr -> use, us, user
The value of this tag appears to be misspelled. Please double-check.

eqp.src: W: spelling-error %description -l en_US robbins -> ribbons, Robbins, robins
The value of this tag appears to be misspelled. Please double-check.

eqp.src: I: checking-url http://www.cs.unm.edu/~mccune/eqp/ (timeout 10 seconds)
eqp.src: I: checking-url http://www.cs.unm.edu/~mccune/old-ftp/eqp-09e.tar.gz (timeout 10 seconds)
eqp.i686: I: checking
eqp.i686: W: spelling-error Summary(en_US) prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.i686: W: spelling-error Summary(en_US) equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.i686: W: spelling-error %description -l en_US equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.i686: W: spelling-error %description -l en_US prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.i686: I: checking-url http://www.cs.unm.edu/~mccune/eqp/ (timeout 10 seconds)
eqp.i686: W: no-manual-page-for-binary eqp
Each executable in standard binary directories should have a man page.

eqp.x86_64: I: checking
eqp.x86_64: W: spelling-error Summary(en_US) prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.x86_64: W: spelling-error Summary(en_US) equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.x86_64: W: spelling-error %description -l en_US equational -> equalization, equation, equitation
The value of this tag appears to be misspelled. Please double-check.

eqp.x86_64: W: spelling-error %description -l en_US prover -> prove, rover, proverb
The value of this tag appears to be misspelled. Please double-check.

eqp.x86_64: I: checking-url http://www.cs.unm.edu/~mccune/eqp/ (timeout 10 seconds)
eqp.x86_64: W: no-manual-page-for-binary eqp
Each executable in standard binary directories should have a man page.

eqp-debuginfo.i686: I: checking
eqp-debuginfo.i686: I: checking-url http://www.cs.unm.edu/~mccune/eqp/ (timeout 10 seconds)
eqp-debuginfo.x86_64: I: checking
eqp-debuginfo.x86_64: I: checking-url http://www.cs.unm.edu/~mccune/eqp/ (timeout 10 seconds)
eqp.spec: I: checking-url http://www.cs.unm.edu/~mccune/old-ftp/eqp-09e.tar.gz (timeout 10 seconds)
5 packages and 1 specfiles checked; 0 errors, 16 warnings.

No recognizable issues from rpmlint.

Still one objection: The %defattr line is obsolete, even for EPEL 5. Please remove.


However, under normal circumstances I would assign this review request to me and do a full review. But what's the current state of the licensing issue? Is it safe now to accept the current license declaration as is, or does it need some further action?
Comment 4 John C Peterson 2012-10-08 16:14:03 EDT
(In reply to comment #3)
> 
> Still one objection: The %defattr line is obsolete, even for EPEL 5. Please
> remove.
> 
> 
> However, under normal circumstances I would assign this review request to me
> and do a full review. But what's the current state of the licensing issue?
> Is it safe now to accept the current license declaration as is, or does it
> need some further action?

Hi Mario,

Thanks for taking the time to get involved with my package review.

The folks on fedora legal were not comfortable with parts of the EQP license. They noted there was no specific mention of the right to distribute modified copies of the software, and wanted clarification of that before they would approve it.

Sadly, the EQP author, Bill McCune passed away in May 2011. This certainly makes it more difficult to resolve the copyright issues in question. However, all is not lost. My suspicion is that the legal holder of the copyright is the organization that funded his work.

I was initially a bit discourgaed about all this, but it is certainly worth sending out a few emails to the right folks at Argonne National Labs where Bill was working during most of the development of EQP to see if they can help us with these issues.

For what it's worth, both EQP and Bill's other famous theorem prover, Otter, are packaged in Debian (which takes copyright issues seriously).

John

P.S. I will modify the spec file to incorporate your recommended changes.
Comment 5 Mario Bl├Ąttermann 2012-10-21 14:35:15 EDT
Anyway, I take this for a full review.
Comment 6 John C Peterson 2012-11-01 18:25:56 EDT
Of course, it's not over until 'the fat lady sings", but a bit of encouraging news on the license issue that is currently holding things up with legal.

I managed to get in contact with the group at Argonne National Laboratory where the (now deceased) EQP author was employed during most of the time it was being developed. We had a couple e-mail exchanges, and I think I sucessfully communicated to them what the issues were regarding the copyright. I don't know how long it will take to get clarification, but they have graciously agreed to look into it.

In the meantime, I removed the defattr tag as requested.

Here are the updated SPEC, SRPM files:

Spec URL: http://jcp.fedorapeople.org/eqp.spec
SRPM URL: http://jcp.fedorapeople.org/eqp-09e-3.fc17.src.rpm
Comment 7 Jason Tibbitts 2013-04-28 19:01:51 EDT
As far as I can tell, this is still blocked on legal issues, so adding the FE-Legal blocker.
Comment 8 Tom "spot" Callaway 2013-04-29 10:56:40 EDT
John, if there is anything I can do to help out you or Argonne, just let me know.
Comment 9 James Hogarth 2015-12-03 22:39:39 EST
John is there any progress on cleaning up the legal situation?
Comment 10 John C Peterson 2015-12-04 17:52:14 EST
Hello James,

The short answer is no.

As I noted in my post dated 2012-11-01, I did get into contact with the organization at Argonne National Laboratory (ANL), where the (now deceased) EQP author was employed when the original work was performed.

There wasn't any formal procedure at ANL for the licensing or distribution of software when the code was first released. Consequently, the EQP software is not even in their own database of ANL developed software. They pretty much just gave me pointers to the "license" that is shown on the project home page (links below). I can forward those emails from ANL to anyone who is interested. 

http://www.mcs.anl.gov/research/projects/AR/eqp/
http://www.cs.unm.edu/~mccune/eqp/

If that "license" is not adequate, then the matter should be considered closed. My feeling is that it's highly unlikely ANL will be inclined to provide any further clarification above and beyond that.
Comment 11 Tom "spot" Callaway 2015-12-07 09:22:23 EST
I revisited this issue with the Red Hat Legal team and they feel comfortable with us treating the "license declaration" on the eqp page as a Public Domain declaration. Use License: Public Domain.

Lifting FE-Legal.
Comment 12 Upstream Release Monitoring 2015-12-15 02:38:31 EST
jcp's scratch build of eqp-09e-4.fc23.src.rpm for f23 completed http://koji.fedoraproject.org/koji/taskinfo?taskID=12194820
Comment 13 John C Peterson 2016-01-06 17:06:18 EST
Hello,

I have taken a fresh look at the eqp package now that Fedora Legal has given the green light on the license (see comment 11 above).

I ran fedora-review, and it identified one small problem that I have corrected (added %{?_sparse_mflags} to the make command line to enable parallel builds). I also did some scratch builds (rawhide, f23) to verify that everything still builds correctly.

Mario: Do you still have time to review this package? No big hurry...

Here are the updated SPEC, SRPM files:

Spec URL: http://www.eskimo.com/~jcp/eqp.spec
SRPM URL: http://www.eskimo.com/~jcp/eqp-09e-4.fc23.src.rpm