[MacPorts] #44543: Submission: cvc4, an automated theorem prover for SMT problems
#44543: Submission: cvc4, an automated theorem prover for SMT problems ------------------------+-------------------------------- Reporter: mdeters@… | Owner: macports-tickets@… Type: submission | Status: new Priority: Normal | Milestone: Component: ports | Version: 2.3.1 Keywords: | Port: cvc4 ------------------------+-------------------------------- Submitting a port for the newest stable version of CVC4, an automated theorem prover for SMT. CVC4 is increasingly being depended on for other projects, so for those projects to be packaged for MacPorts, cvc4 will have to be available. We have been using this port internally (and distributed for our users) for some time now, but would like to have it included in . I would be happy to maintain the port, as I am now, for new versions and for fixes to the packaging. The only somewhat ugly thing about this portfile is that it downloads and (statically) links in a dependence (the antlr C library). This functionality would best be provided as a separate port (but isn't available currently). I'd be willing to work with someone to create a suitable antlr-C port if that would be beneficial to the MacPorts community. I'd be interested in any feedback, especially suggested improvements. The package is "port lint"-clean. I also have a (substantially similar) "cvc4-devel" port, which could be included also, which tracks our nightly development snapshot. -- Ticket URL: <https://trac.macports.org/ticket/44543> MacPorts <http://www.macports.org/> Ports system for OS X
#44543: Submission: cvc4, an automated theorem prover for SMT problems -------------------------+-------------------------------- Reporter: mdeters@… | Owner: macports-tickets@… Type: submission | Status: new Priority: Normal | Milestone: Component: ports | Version: 2.3.1 Resolution: | Keywords: Port: cvc4 | -------------------------+-------------------------------- Comment (by ryandesign@…): Thanks. Some observations: * The standard modeline should be inserted before line 1. * The line "`distname cvc4-${version}`" should be deleted because that is the default value. * We don't want to add variants whose names begin with "no" anymore. Why is the "no_static" variant needed or desired? What harm is there to always installing both static and dynamic libraries, which is what we would like all ports to do if possible? * In the debug variant, instead of invoking both "`configure.args- delete`" and" `configure.args-append`", consider using "`configure.args- replace`" instead. -- Ticket URL: <https://trac.macports.org/ticket/44543#comment:1> MacPorts <http://www.macports.org/> Ports system for OS X
#44543: Submission: cvc4, an automated theorem prover for SMT problems -------------------------+-------------------------------- Reporter: mdeters@… | Owner: macports-tickets@… Type: submission | Status: new Priority: Normal | Milestone: Component: ports | Version: 2.3.1 Resolution: | Keywords: Port: cvc4 | -------------------------+-------------------------------- Comment (by mdeters@…): Thanks for the comments. I have corrected the Portfile, but first a question. If I build static libraries, the installation size goes up dramatically. We had complaints from users that the (mpkg) installers were large (~125MB) so I added +no_static and now they are ~6MB. Size on disk is also an issue (the largest of our static libs, libcvc4.a, is 648 MB). Is there a good way of dealing with this without using a variant? -- Ticket URL: <https://trac.macports.org/ticket/44543#comment:2> MacPorts <http://www.macports.org/> Ports system for OS X
#44543: Submission: cvc4, an automated theorem prover for SMT problems -------------------------+-------------------------------- Reporter: mdeters@… | Owner: macports-tickets@… Type: submission | Status: new Priority: Normal | Milestone: Component: ports | Version: 2.3.1 Resolution: | Keywords: Port: cvc4 | -------------------------+-------------------------------- Comment (by mdeters@…): Replying to [comment:2 mdeters@…]:
Size on disk is also an issue (the largest of our static libs, libcvc4.a, is 648 MB). Is there a good way of dealing with this without using a variant?
One way I can work around this is to override "destroot" and force a "make install-strip" instead of "make install". Is doing so acceptable for MacPorts? I'm attaching an updated Portfile. -- Ticket URL: <https://trac.macports.org/ticket/44543#comment:3> MacPorts <http://www.macports.org/> Ports system for OS X
#44543: Submission: cvc4, an automated theorem prover for SMT problems -------------------------+-------------------------------- Reporter: mdeters@… | Owner: macports-tickets@… Type: submission | Status: closed Priority: Normal | Milestone: Component: ports | Version: 2.3.1 Resolution: fixed | Keywords: Port: cvc4 | -------------------------+-------------------------------- Changes (by khindenburg@…): * status: new => closed * resolution: => fixed Comment: thanks - added r124908 I removed the revision since this is a new port; and the conflicts since the -devel doesn't exist ATM. -- Ticket URL: <https://trac.macports.org/ticket/44543#comment:5> MacPorts <http://www.macports.org/> Ports system for OS X
participants (1)
-
MacPorts