Submission: cvc4, an automated theorem prover for SMT problems

[mdeters@…]

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.

[ryandesign (Ryan Carsten Schmidt)]

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.

[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?

[mdeters@…]

Replying to 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.

[mdeters@…]

updated Portfile for cvc4

[kurthindenburg (Kurt Hindenburg)]

Cc Me!

[kurthindenburg (Kurt Hindenburg)]

thanks - added r124908

I removed the revision since this is a new port; and the conflicts since the -devel doesn't exist ATM.