Opened 6 years ago

Closed 5 years ago

#44543 closed submission (fixed)

Submission: cvc4, an automated theorem prover for SMT problems

Reported by: mdeters@… Owned by: macports-tickets@…
Priority: Normal Milestone:
Component: ports Version: 2.3.1
Keywords: Cc: kurthindenburg (Kurt Hindenburg)
Port: cvc4

Description

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.

Attachments (1)

Portfile (2.8 KB) - added by mdeters@… 6 years ago.
updated Portfile for cvc4

Download all attachments as: .zip

Change History (6)

comment:1 Changed 6 years ago by ryandesign (Ryan 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.

comment:2 Changed 6 years ago 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?

comment:3 in reply to:  2 Changed 6 years ago by 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.

Changed 6 years ago by mdeters@…

Attachment: Portfile added

updated Portfile for cvc4

comment:4 Changed 5 years ago by kurthindenburg (Kurt Hindenburg)

Cc: khindenburg@… added

Cc Me!

comment:5 Changed 5 years ago by kurthindenburg (Kurt Hindenburg)

Resolution: fixed
Status: newclosed

thanks - added r124908

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

Note: See TracTickets for help on using tickets.