Attached you find the ebuild and patch necessary to build Mace4. The ebuild also supports Intels compiler, USE="icc" Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than Mace2 which is bundled in app-sci/otter-3.3. Thomas Reproducible: Always Steps to Reproduce: 1. 2. 3.
Created attachment 30177 [details] mace4-2003b.ebuild This ebuild and the attached patch build on my box, regression stable in gcc 3.3.3 and icc 8.0.
Created attachment 30178 [details, diff] gentoo-mace4.patch This patch allows to use user specified CFLAGS from make.conf and allows mace to be built with intel c compiler
*** Bug 233476 has been marked as a duplicate of this bug. ***
(this is an automated message based on filtering criteria that matched this bug) Hello, The Gentoo Team would like to firstly thank you for your ebuild submission. We also apologize for not being able to accommodate you in a timely manner. There are simply too many new packages. Allow me to use this opportunity to introduce you to Gentoo Sunrise. The sunrise overlay[1] is a overlay for Gentoo which we allow trusted users to commit to and all users can have ebuilds reviewed by Gentoo devs for entry into the overlay. So, the sunrise team is suggesting that you look into this and submit your ebuild to the overlay where even *you* can commit to. =) Because this is a mass message, we are also asking you to be patient with us. We anticipate a large number of requests in a short time. Thanks, On behalf of the Gentoo Sunrise Team, Jeremy. [1]: http://www.gentoo.org/proj/en/sunrise/ [2]: http://overlays.gentoo.org/proj/sunrise/wiki/SunriseFaq
Created attachment 298183 [details] prover9 mace4 ebuild I will commit this to the cvs portage tree, adding the ebuild to the patch first in case someone wants to review it.
Created attachment 298185 [details] makefile patch to use our CFLAGS, build library with -fpic
Created attachment 298187 [details] manpages patch (thanks debian)
Created attachment 298189 [details] sci-mathematics/prover9 metadata
sci-mathematics/prover9-2009.11a added to portage.