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

[yuri]

Summary

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

[tcberner]

math/eprover/Makefile

33 ↗

(On Diff #35441)

^ this could use a line-break

[tcberner]

I see the following error

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

[yuri]

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?

[yuri]

Added the line-break.

[tcberner]

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.

[yuri]

Backported the fix.

[yuri]

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

[tcberner]

In D13150#273828, @yuri wrote:

Backported the fix.

good job

[yuri]

In D13150#274063, @tcberner wrote:

In D13150#273828, @yuri wrote:

Backported the fix.

good job

Thanks

[mat]

head/math/eprover/Makefile

23–24

Is this really needed ? Wouldn't USES=desthack work ?

[yuri]

head/math/eprover/Makefile

23–24

It breaks with USES=desthack:

strip: open /usr/ports/math/eprover/work/stage/usr/local/bin/checkproof failed: No such file or directory