Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 49205 - app-sci/mace4-2003b.ebuild (new package)
Summary: app-sci/mace4-2003b.ebuild (new package)
Status: RESOLVED FIXED
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: New packages (show other bugs)
Hardware: All Linux
: High enhancement (vote)
Assignee: Mark Wright
URL: http://www-unix.mcs.anl.gov/AR/mace4
Whiteboard: sunrise suggested
Keywords: EBUILD
: 233476 (view as bug list)
Depends on:
Blocks:
 
Reported: 2004-04-27 14:17 UTC by Thomas Veith (RETIRED)
Modified: 2012-01-08 13:59 UTC (History)
1 user (show)

See Also:
Package list:
Runtime testing required: ---


Attachments
mace4-2003b.ebuild (mace4-2003b.ebuild,1.54 KB, text/plain)
2004-04-27 14:20 UTC, Thomas Veith (RETIRED)
Details
gentoo-mace4.patch (gentoo-mace4.patch,1.13 KB, patch)
2004-04-27 14:21 UTC, Thomas Veith (RETIRED)
Details | Diff
prover9 mace4 ebuild (prover9-2009.11a.ebuild,4.49 KB, text/plain)
2012-01-07 10:38 UTC, Mark Wright
Details
makefile patch to use our CFLAGS, build library with -fpic (LADR-2009-11A-makefile.patch,42.50 KB, text/plain)
2012-01-07 10:41 UTC, Mark Wright
Details
manpages patch (thanks debian) (LADR-2009-11A-manpages.patch,13.51 KB, text/plain)
2012-01-07 10:42 UTC, Mark Wright
Details
sci-mathematics/prover9 metadata (metadata.xml,423 bytes, text/plain)
2012-01-07 10:43 UTC, Mark Wright
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Thomas Veith (RETIRED) gentoo-dev 2004-04-27 14:17:54 UTC
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.
Comment 1 Thomas Veith (RETIRED) gentoo-dev 2004-04-27 14:20:12 UTC
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.
Comment 2 Thomas Veith (RETIRED) gentoo-dev 2004-04-27 14:21:42 UTC
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
Comment 3 Carsten Lohrke (RETIRED) gentoo-dev 2008-08-01 09:53:47 UTC
*** Bug 233476 has been marked as a duplicate of this bug. ***
Comment 4 Jeremy Olexa (darkside) (RETIRED) archtester gentoo-dev Security 2009-01-07 17:13:02 UTC
(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
Comment 5 Mark Wright gentoo-dev 2012-01-07 10:38:34 UTC
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.
Comment 6 Mark Wright gentoo-dev 2012-01-07 10:41:40 UTC
Created attachment 298185 [details]
makefile patch to use our CFLAGS, build library with -fpic
Comment 7 Mark Wright gentoo-dev 2012-01-07 10:42:32 UTC
Created attachment 298187 [details]
manpages patch (thanks debian)
Comment 8 Mark Wright gentoo-dev 2012-01-07 10:43:47 UTC
Created attachment 298189 [details]
sci-mathematics/prover9 metadata
Comment 9 Mark Wright gentoo-dev 2012-01-08 13:59:12 UTC
sci-mathematics/prover9-2009.11a added to portage.