New port: math/eprover : Theorem prover for full first-order logic with equality
ClosedPublic
Actions

Authored by yuri on Nov 18 2017, 10:01 PM.

Details

Reviewers

tcberner
adamw

Commits

rP454506: New port: math/eprover : Theorem prover for full first-order logic with equality

Summary

https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=211903

Diff Detail

Repository

rP FreeBSD ports repository

Lint

No Lint Coverage

Unit

No Test Coverage

Build Status

Buildable 12847
Build 13111: arc lint + arc unit

Event Timeline

yuri created this revision.Nov 18 2017, 10:01 PM

Herald added a subscriber: mat. · View Herald TranscriptNov 18 2017, 10:01 PM

tcberner added inline comments.Nov 18 2017, 10:07 PM

math/eprover/Makefile
33	^ this could use a line-break

I see the following error

cp: DOC/man/e_deduction_server.1: No such file or directory
*** Error code 1 (ignored)

In D13150#273821, @tcberner wrote:
I see the following error
cp: DOC/man/e_deduction_server.1: No such file or directory
*** Error code 1 (ignored)

This error was fixed later, and doesn't break the build.
So we need to patch it, or just wait for the next release?

Added the line-break.

Harbormaster completed remote builds in B12848: Diff 35442.Nov 18 2017, 10:22 PM

In D13150#273822, @yuri wrote:
In D13150#273821, @tcberner wrote:
I see the following error
cp: DOC/man/e_deduction_server.1: No such file or directory
*** Error code 1 (ignored)
This error was fixed later, and doesn't break the build.
So we need to patch it, or just wait for the next release?

If you can back port the fix without much effort I would go for it. Otherwise it can wait.

Backported the fix.

Harbormaster completed remote builds in B12849: Diff 35443.Nov 18 2017, 10:52 PM

The author, professor from Germany, actually answered my e-mail about this error. :)

In D13150#273828, @yuri wrote:

Backported the fix.

good job

tcberner accepted this revision.Nov 19 2017, 9:54 PM

This revision is now accepted and ready to land.Nov 19 2017, 9:54 PM

In D13150#274063, @tcberner wrote:

In D13150#273828, @yuri wrote:

Backported the fix.

good job

Thanks

Closed by commit rP454506: New port: math/eprover : Theorem prover for full first-order logic with equality (authored by yuri). · Explain WhyNov 19 2017, 9:59 PM

This revision was automatically updated to reflect the committed changes.

mat added inline comments.Nov 24 2017, 5:57 PM

head/math/eprover/Makefile
23–24 ↗	(On Diff #35477)	Is this really needed ? Wouldn't `USES=desthack` work ?

yuri marked an inline comment as done.Nov 24 2017, 8:45 PM

yuri added inline comments.

head/math/eprover/Makefile
23–24 ↗	(On Diff #35477)	It breaks with `USES=desthack`: strip: open /usr/ports/math/eprover/work/stage/usr/local/bin/checkproof failed: No such file or directory