Created attachment 173738 [details] Eprover port E is a theorem prover for full first-order logic with equality.
Hi, The build failed with the message: =======================<phase: configure >============================ ===> Configuring for eprover-1.9 Configuring with executable path /wrkdirs/usr/ports/math/eprover/work/stage/usr/local/bin/ /wrkdirs/usr/ports/math/eprover/work/stage/usr/local/man/man1/ echo 'Configuring build system and tools' Configuring build system and tools make links cd include; touch does_exist.h; rm *.h cd lib; touch does_exist.a; rm *.a cd include; for subdir in BASICS INOUT TERMS ORDERINGS CLAUSES PROPOSITIONAL LEARN ANALYSIS PCL2 HEURISTICS CONTROL EXTERNAL PROVER; do for file in ../$subdir/*.h; do ln -s $file .; done; done; cd lib; for subdir in BASICS INOUT TERMS ORDERINGS CLAUSES PROPOSITIONAL LEARN ANALYSIS PCL2 HEURISTICS CONTROL; do ln -s ../$subdir/$subdir.a .; done; make tools cd development_tools;make tools Configuring tools ./configure_tools Using tail -n Your which command works! /usr/bin/awk configure_tools: Cannot find gawk, trying awk (untested) configure_tools: No Python available, tools unconfigured. configure_tools: Try to get Python 2.X installed in your search path. ./configure_bash_scripts configure_bash_scripts: Cannot find bash, trying /bin/sh (untested) cd PYTHON; make tools Configuring tools ../development_tools/configure_tools Using tail -n Your which command works! /usr/bin/awk configure_tools: Cannot find gawk, trying awk (untested) configure_tools: No Python available, tools unconfigured. configure_tools: Try to get Python 2.X installed in your search path. make depend for subdir in BASICS INOUT TERMS ORDERINGS CLAUSES PROPOSITIONAL LEARN ANALYSIS PCL2 HEURISTICS CONTROL PROVER TEST SIMPLE_APPS EXTERNAL; do cd $subdir; touch Makefile.dependencies; make depend; cd ..; done; gcc -M -O4 -fomit-frame-pointer -Wall -std=gnu99 -I../include -DNDEBUG -DFAST_EXIT -DPRINT_SOMEERRORS_STDOUT -DMEMORY_RESERVE_PARANOID -DPRINT_TSTP_STATUS -DSTACK_SIZE=32768 -DCLAUSE_PERM_IDENT *.c > Makefile.dependencies /bin/sh: gcc: not found *** Error code 127 Stop. make[3]: stopped in /wrkdirs/usr/ports/math/eprover/work/E/BASICS *** Error code 1 Stop. make[2]: stopped in /wrkdirs/usr/ports/math/eprover/work/E *** Error code 1 Stop. make[1]: stopped in /wrkdirs/usr/ports/math/eprover/work/E Would you test it again ? wen
Created attachment 174011 [details] Eprover port (added gcc dep)
(In reply to Wen Heping from comment #1) Hi Wen, Sorry about that. This is my first port, I've forgotten to add gcc as a dependency. It should work now. Cheers, Victor
(In reply to Victor Gomes from comment #3) Adding GCC as a dependency is wrong if clang can compile it. You need to first patch it and see it if works with clang.
Version 2.0 is available.
Other items to fix: * EXTRACT_SFX needs to be replaced with USES=tar:tgz * You can't patch "PREFIX=/usr/local/bin" into configure. This has to work through the environment variable, and has to be based on ${PREFIX} variable * The rest of configure patch needs to be in Makefile (post-patch, REINPLACE_CMD, etc) * patch-PROVER_eproof__ram needs to be replaced with USES=shebangfix * USE_GCC=any not needed unless it doesn't build with clang. * HAS_CONFIGURE needs to be replaced with GNU_CONFIGURE=yes * --man-prefix= can't include /usr/local, it should be ${PREFIX} Thanks!
Some more items: * It should be called just 'e', because the author calls it this. * The port name can be 'E', I think, so that it will reflect how it is known. Regards, Yuri
Created attachment 187373 [details] eprover.patch (alternative variant) Here's my version of the port. (Didn't search bugzilla before writing the port… :D) Uses version 2.0. GNU_CONFIGURE will not work, configure here is NOT GNU configure, it's a custom script. GNU_CONFIGURE passes unsupported options. It's called "eprover" in Arch Linux AUR and Mac Homebrew. Everyone refers to it as "eprover" because that's how the binary is called, and "E" is an ungooglable name. It's like "golang" instead of "Go".
(In reply to Greg V from comment #8) Greg, Thanks for your submission.
It has 2 problems: * Build hangs in the 10i386 machine for some reason * Build also fails in the 11amd64 machine in the manpage generation phase
(In reply to Yuri Victorovich from comment #10) How exactly does manpage generation fail? o_0 It's just help2man, works fine on my 12amd64 machine.
(In reply to Greg V from comment #11) On 11amd64 it fails like this: > help2man -N -i DOC/bug_reporting PROVER/eproof > DOC/man/eproof.1 > help2man: can't get `--help' info from PROVER/eproof > Try `--no-discard-stderr' if option outputs to stderr > *** Error code 127
Created attachment 188101 [details] Modified Greg's eprover.patch I changed it a bit.
Created attachment 188102 [details] Modified Greg's eprover.patch
(In reply to Yuri Victorovich from comment #12) hmmm, does the eproof binary that it's trying to run actually work?
(In reply to Greg V from comment #15) Oh, eproof is a shell script, right
(In reply to Greg V from comment #16) Ok, thanks, I will fix this.
A commit references this bug: Author: yuri Date: Sun Nov 19 21:59:33 UTC 2017 New revision: 454506 URL: https://svnweb.freebsd.org/changeset/ports/454506 Log: New port: math/eprover : Theorem prover for full first-order logic with equality PR: 211903 Submitted by: Greg V <greg@unrelenting.technology> Approved by: tcberner (mentor) Differential Revision: https://reviews.freebsd.org/D13150 Changes: head/math/Makefile head/math/eprover/ head/math/eprover/Makefile head/math/eprover/distinfo head/math/eprover/files/ head/math/eprover/files/patch-Makefile head/math/eprover/files/patch-Makefile.vars head/math/eprover/pkg-descr head/math/eprover/pkg-plist
Committed with some changes. Thanks!