No rule to make target `libladr.a'.

516> git branch

makefile master paul@leonardo:~/sources/ladr 517> ls total 312 -rw-r--r-- 1 paul staff 17987 May 17 23:15 COPYING -rw-r--r-- 1 paul staff 62287 May 17 23:15 Changelog -rw-r--r-- 1 paul staff 1492 May 17 23:15 Makefile -rw-r--r-- 1 paul staff 913 May 17 23:15 README.AMD_64 -rw-r--r-- 1 paul staff 162 May 17 23:15 README.first -rw-r--r-- 1 paul staff 610 May 17 23:15 README.make -rw-r--r-- 1 paul staff 290 May 17 23:15 README.release-reminder drwxr-xr-x 7 paul staff 238 May 17 23:15 TODO/ -rw-r--r-- 1 paul staff 78 May 17 23:15 VERSIONDATE.h drwxr-xr-x 22 paul staff 748 May 17 23:15 apps.examples/ drwxr-xr-x 56 paul staff 1904 May 17 23:15 apps.src/ drwxr-xr-x 7 paul staff 238 May 17 23:15 bob/ drwxr-xr-x 29 paul staff 986 May 17 23:25 ladr/ -rw-r--r-- 1 paul staff 38551 May 17 23:15 libtoolize.patch drwxr-xr-x 5 paul staff 170 May 17 23:15 mace4.examples/ drwxr-xr-x 41 paul staff 1394 May 17 23:15 mace4.src/ drwxr-xr-x 4 paul staff 136 May 17 23:15 manpages/ drwxr-xr-x 6 paul staff 204 May 17 23:15 prover9.examples/ drwxr-xr-x 56 paul staff 1904 May 17 23:15 provers.src/ -rwxr-xr-x 1 paul staff 343 May 17 23:15 rev.py* -rw-r--r-- 1 paul staff 775 May 17 23:15 sed.gnu-blurb drwxr-xr-x 11 paul staff 374 May 17 23:15 test.src/ drwxr-xr-x 10 paul staff 340 May 17 23:15 utilities/ drwxr-xr-x 9 paul staff 306 May 17 23:15 utilities-old/ paul@leonardo:~/sources/ladr 518> make clean cd ladr && make realclean make clean cd ladr && make realclean /bin/rm -f .o .a cd apps.src && make realclean /bin/rm -f .o latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs cd mace4.src && make realclean /bin/rm -f .o .a mace4 cd provers.src && make realclean /bin/rm -f .o prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_toladr /bin/rm -f bin/ cd apps.src && make realclean /bin/rm -f _.o latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs cd mace4.src && make realclean /bin/rm -f .o .a mace4 cd provers.src && make realclean /bin/rm -f .o prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr paul@leonardo:~/sources/ladr 519> make all cd ladr && make lib cd ladr && make lib make libladr.a gcc -O -Wall -c -o order.o order.c gcc -O -Wall -c -o clock.o clock.c gcc -O -Wall -c -o nonport.o nonport.c gcc -O -Wall -c -o fatal.o fatal.c gcc -O -Wall -c -o ibuffer.o ibuffer.c gcc -O -Wall -c -o memory.o memory.c gcc -O -Wall -c -o hash.o hash.c gcc -O -Wall -c -o string.o string.c gcc -O -Wall -c -o strbuf.o strbuf.c gcc -O -Wall -c -o glist.o glist.c gcc -O -Wall -c -o options.o options.c gcc -O -Wall -c -o symbols.o symbols.c gcc -O -Wall -c -o avltree.o avltree.c avltree.c: In function ‘p_avl’: avltree.c:658: warning: cast from pointer to integer of different size gcc -O -Wall -c -o term.o term.c gcc -O -Wall -c -o termflag.o termflag.c gcc -O -Wall -c -o listterm.o listterm.c gcc -O -Wall -c -o tlist.o tlist.c gcc -O -Wall -c -o flatterm.o flatterm.c gcc -O -Wall -c -o multiset.o multiset.c gcc -O -Wall -c -o termorder.o termorder.c gcc -O -Wall -c -o parse.o parse.c gcc -O -Wall -c -o accanon.o accanon.c gcc -O -Wall -c -o unify.o unify.c gcc -O -Wall -c -o fpalist.o fpalist.c gcc -O -Wall -c -o fpa.o fpa.c gcc -O -Wall -c -o discrim.o discrim.c gcc -O -Wall -c -o discrimb.o discrimb.c gcc -O -Wall -c -o discrimw.o discrimw.c gcc -O -Wall -c -o dioph.o dioph.c gcc -O -Wall -c -o btu.o btu.c gcc -O -Wall -c -o btm.o btm.c gcc -O -Wall -c -o mindex.o mindex.c gcc -O -Wall -c -o basic.o basic.c gcc -O -Wall -c -o attrib.o attrib.c gcc -O -Wall -c -o formula.o formula.c gcc -O -Wall -c -o definitions.o definitions.c gcc -O -Wall -c -o literals.o literals.c gcc -O -Wall -c -o topform.o topform.c gcc -O -Wall -c -o clist.o clist.c gcc -O -Wall -c -o clauseid.o clauseid.c gcc -O -Wall -c -o clauses.o clauses.c gcc -O -Wall -c -o just.o just.c gcc -O -Wall -c -o cnf.o cnf.c gcc -O -Wall -c -o clausify.o clausify.c gcc -O -Wall -c -o parautil.o parautil.c gcc -O -Wall -c -o pindex.o pindex.c gcc -O -Wall -c -o compress.o compress.c gcc -O -Wall -c -o maximal.o maximal.c gcc -O -Wall -c -o lindex.o lindex.c gcc -O -Wall -c -o weight.o weight.c gcc -O -Wall -c -o weight2.o weight2.c gcc -O -Wall -c -o int_code.o int_code.c gcc -O -Wall -c -o features.o features.c gcc -O -Wall -c -o di_tree.o di_tree.c gcc -O -Wall -c -o fastparse.o fastparse.c fastparse.c: In function ‘fast_read_term’: fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments gcc -O -Wall -c -o random.o random.c gcc -O -Wall -c -o subsume.o subsume.c gcc -O -Wall -c -o clause_misc.o clause_misc.c gcc -O -Wall -c -o clause_eval.o clause_eval.c gcc -O -Wall -c -o complex.o complex.c gcc -O -Wall -c -o dollar.o dollar.c gcc -O -Wall -c -o flatdemod.o flatdemod.c gcc -O -Wall -c -o demod.o demod.c gcc -O -Wall -c -o clash.o clash.c gcc -O -Wall -c -o resolve.o resolve.c gcc -O -Wall -c -o paramod.o paramod.c gcc -O -Wall -c -o backdemod.o backdemod.c gcc -O -Wall -c -o hints.o hints.c gcc -O -Wall -c -o ac_redun.o ac_redun.c gcc -O -Wall -c -o xproofs.o xproofs.c gcc -O -Wall -c -o ivy.o ivy.c gcc -O -Wall -c -o interp.o interp.c gcc -O -Wall -c -o std_options.o std_options.c gcc -O -Wall -c -o banner.o banner.c gcc -O -Wall -c -o ioutil.o ioutil.c gcc -O -Wall -c -o tptp_trans.o tptp_trans.c gcc -O -Wall -c -o top_input.o top_input.c ar rs libladr.a order.o clock.o nonport.o fatal.o ibuffer.o memory.o hash.o string.o strbuf.o glist.o options.o symbols.o avltree.o term.o termflag.o listterm.o tlist.o flatterm.o multiset.o termorder.o parse.o accanon.o unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o dioph.o btu.o btm.o mindex.o basic.o attrib.o formula.o definitions.o literals.o topform.o clist.o clauseid.o clauses.o just.o cnf.o clausify.o parautil.o pindex.o compress.o maximal.o lindex.o weight.o weight2.o int_code.o features.o di_tree.o fastparse.o random.o subsume.o clause_misc.o clause_eval.o complex.o dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o backdemod.o hints.o ac_redun.o xproofs.o ivy.o interp.o std_options.o banner.o ioutil.o tptp_trans.o topinput.o ar: creating archive libladr.a cd mace4.src && make all cd ../ladr && make libladr.a make[2]: ** No rule to make target `libladr.a'. Stop. make[1]: * [ladr] Error 2 make: * [all] Error 2 paul@leonardo:~/sources/ladr 520>

Thanks for reporting the bug. I've done some work on this issue. Can you check out the latest on the 'makefile' branch and try again? (Make sure to do a 'make clean' before proceeding.) It works for me, but I want to confirm that it works for you before closing this issue. Thanks for the detailed output.

Pulled the branch using the github app. 7353295656600e3fada12bc1d034680d5ca1375b was the last commit. make clean succeeded; make all resulted in an error, transcript appended. If this email doesn't create a reply on github, I'll respond there as well.

Last login: Fri May 18 10:32:43 on ttys000 paul@leonardo:~ 501> cd sources/ladr paul@leonardo:~/sources/ladr 502> make clean make -C ladr realclean make clean cd ladr && make realclean /bin/rm -f _.o .a cd apps.src && make realclean /bin/rm -f .o latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs cd mace4.src && make realclean /bin/rm -f .o .a mace4 cd provers.src && make realclean /bin/rm -f .o prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_toladr /bin/rm -f bin/ make -C apps.src realclean /bin/rm -f _.o latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs make -C mace4.src realclean /bin/rm -f .o .a mace4 make -C provers.src realclean /bin/rm -f .o prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr paul@leonardo:~/sources/ladr 503> make all make -C ladr lib cd ladr && make lib make libladr.a gcc -O -Wall -c -o order.o order.c gcc -O -Wall -c -o clock.o clock.c gcc -O -Wall -c -o nonport.o nonport.c gcc -O -Wall -c -o fatal.o fatal.c gcc -O -Wall -c -o ibuffer.o ibuffer.c gcc -O -Wall -c -o memory.o memory.c gcc -O -Wall -c -o hash.o hash.c gcc -O -Wall -c -o string.o string.c gcc -O -Wall -c -o strbuf.o strbuf.c gcc -O -Wall -c -o glist.o glist.c gcc -O -Wall -c -o options.o options.c gcc -O -Wall -c -o symbols.o symbols.c gcc -O -Wall -c -o avltree.o avltree.c avltree.c: In function ‘p_avl’: avltree.c:658: warning: cast from pointer to integer of different size gcc -O -Wall -c -o term.o term.c gcc -O -Wall -c -o termflag.o termflag.c gcc -O -Wall -c -o listterm.o listterm.c gcc -O -Wall -c -o tlist.o tlist.c gcc -O -Wall -c -o flatterm.o flatterm.c gcc -O -Wall -c -o multiset.o multiset.c gcc -O -Wall -c -o termorder.o termorder.c gcc -O -Wall -c -o parse.o parse.c gcc -O -Wall -c -o accanon.o accanon.c gcc -O -Wall -c -o unify.o unify.c gcc -O -Wall -c -o fpalist.o fpalist.c gcc -O -Wall -c -o fpa.o fpa.c gcc -O -Wall -c -o discrim.o discrim.c gcc -O -Wall -c -o discrimb.o discrimb.c gcc -O -Wall -c -o discrimw.o discrimw.c gcc -O -Wall -c -o dioph.o dioph.c gcc -O -Wall -c -o btu.o btu.c gcc -O -Wall -c -o btm.o btm.c gcc -O -Wall -c -o mindex.o mindex.c gcc -O -Wall -c -o basic.o basic.c gcc -O -Wall -c -o attrib.o attrib.c gcc -O -Wall -c -o formula.o formula.c gcc -O -Wall -c -o definitions.o definitions.c gcc -O -Wall -c -o literals.o literals.c gcc -O -Wall -c -o topform.o topform.c gcc -O -Wall -c -o clist.o clist.c gcc -O -Wall -c -o clauseid.o clauseid.c gcc -O -Wall -c -o clauses.o clauses.c gcc -O -Wall -c -o just.o just.c gcc -O -Wall -c -o cnf.o cnf.c gcc -O -Wall -c -o clausify.o clausify.c gcc -O -Wall -c -o parautil.o parautil.c gcc -O -Wall -c -o pindex.o pindex.c gcc -O -Wall -c -o compress.o compress.c gcc -O -Wall -c -o maximal.o maximal.c gcc -O -Wall -c -o lindex.o lindex.c gcc -O -Wall -c -o weight.o weight.c gcc -O -Wall -c -o weight2.o weight2.c gcc -O -Wall -c -o int_code.o int_code.c gcc -O -Wall -c -o features.o features.c gcc -O -Wall -c -o di_tree.o di_tree.c gcc -O -Wall -c -o fastparse.o fastparse.c fastparse.c: In function ‘fast_read_term’: fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments gcc -O -Wall -c -o random.o random.c gcc -O -Wall -c -o subsume.o subsume.c gcc -O -Wall -c -o clause_misc.o clause_misc.c gcc -O -Wall -c -o clause_eval.o clause_eval.c gcc -O -Wall -c -o complex.o complex.c gcc -O -Wall -c -o dollar.o dollar.c gcc -O -Wall -c -o flatdemod.o flatdemod.c gcc -O -Wall -c -o demod.o demod.c gcc -O -Wall -c -o clash.o clash.c gcc -O -Wall -c -o resolve.o resolve.c gcc -O -Wall -c -o paramod.o paramod.c gcc -O -Wall -c -o backdemod.o backdemod.c gcc -O -Wall -c -o hints.o hints.c gcc -O -Wall -c -o ac_redun.o ac_redun.c gcc -O -Wall -c -o xproofs.o xproofs.c gcc -O -Wall -c -o ivy.o ivy.c gcc -O -Wall -c -o interp.o interp.c gcc -O -Wall -c -o std_options.o std_options.c gcc -O -Wall -c -o banner.o banner.c gcc -O -Wall -c -o ioutil.o ioutil.c gcc -O -Wall -c -o tptp_trans.o tptp_trans.c gcc -O -Wall -c -o top_input.o top_input.c ar rs libladr.a order.o clock.o nonport.o fatal.o ibuffer.o memory.o hash.o string.o strbuf.o glist.o options.o symbols.o avltree.o term.o termflag.o listterm.o tlist.o flatterm.o multiset.o termorder.o parse.o accanon.o unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o dioph.o btu.o btm.o mindex.o basic.o attrib.o formula.o definitions.o literals.o topform.o clist.o clauseid.o clauses.o just.o cnf.o clausify.o parautil.o pindex.o compress.o maximal.o lindex.o weight.o weight2.o int_code.o features.o di_tree.o fastparse.o random.o subsume.o clause_misc.o clause_eval.o complex.o dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o backdemod.o hints.o ac_redun.o xproofs.o ivy.o interp.o std_options.o banner.o ioutil.o tptp_trans.o topinput.o ar: creating archive libladr.a make -C mace4.src cd ../ladr && make libladr.a make[2]: ** No rule to make target `libladr.a'. Stop. make[1]: * [ladr] Error 2 make: * [all] Error 2 paul@leonardo:~/sources/ladr 504> On May 18, 2012, at 2:53 AM, Jesse Alama wrote:

Thanks for reporting the bug. I've done some work on this issue. Can you check out the latest on the 'makefile' branch and try again? (Make sure to do a 'make clean' before proceeding.) It works for me, but I want to confirm that it works for you before closing this issue. Thanks for the detailed output.

Reply to this email directly or view it on GitHub: https://github.com/jessealama/ladr/issues/1#issuecomment-5782812

Can you please pull the latest commits in the makefile branch and try again? Commit 80e96f332dbe8815135a815fa903492d19c5f840 on my machine seems to work. One way to test all this is to kill everything in the ladr repo, except the .git directory, and then do

    git checkout --force makefile

and then

    make all

I don't trust that make clean kills everything.

I removed the ladr directory completely, and started over from scratch. make all still fails. Transcript follows. Thanks!

Last login: Sat May 19 11:50:02 on ttys000 paul@leonardo:~ 501> cd sources paul@leonardo:~/sources 502> ls total 0 drwxr-xr-x@ 35 paul staff 1190 May 9 15:26 E/ drwxr-xr-x 39 paul staff 1326 May 9 04:06 dialogues/ drwxr-xr-x 7 paul staff 238 May 9 04:36 dotemacs/ drwxr-xr-x 15 paul staff 510 May 9 03:48 mizar-parser/ drwx------ 16 paul staff 544 Apr 26 02:35 tipi/ drwxr-xr-x 12 paul staff 408 May 9 03:46 tptp4mizar/ paul@leonardo:~/sources 503> history | grep git 57 $ git show HEAD | head -n 1 58 git show HEAD | head -n 1 59 git show HEAD | head -n 1 202 git clone git://github.com/mkoconnor/John-Harrison-s-Automated-Reasoning-Code.git 213 git status 433 git log 435 git log 436 git branch 452 open https://github.com/ 455 git --help 456 git branch 457 git branch 458 git branch makefile 459 git branch 460 git putll 461 git pull 462 git status 463 man git 464 open http://www.kernel.org/pub/software/scm/git/docs/howto-index.html 465 git checkout makefile 467 git branch 503 history | grep git paul@leonardo:~/sources 504> date Sat May 19 13:13:34 MST 2012 paul@leonardo:~/sources 505> git clone https://jessealama@github.com/jessealama/ladr.git Cloning into ladr... Password: remote: Counting objects: 733, done. remote: Compressing objects: 100% (554/554), done. remote: Total 733 (delta 186), reused 716 (delta 169) Receiving objects: 100% (733/733), 1.73 MiB | 677 KiB/s, done. Resolving deltas: 100% (186/186), done. paul@leonardo:~/sources 506> ls total 0 drwxr-xr-x@ 35 paul staff 1190 May 9 15:26 E/ drwxr-xr-x 39 paul staff 1326 May 9 04:06 dialogues/ drwxr-xr-x 7 paul staff 238 May 9 04:36 dotemacs/ drwx------ 29 paul staff 986 May 19 13:16 ladr/ drwxr-xr-x 15 paul staff 510 May 9 03:48 mizar-parser/ drwx------ 16 paul staff 544 Apr 26 02:35 tipi/ drwxr-xr-x 12 paul staff 408 May 9 03:46 tptp4mizar/ paul@leonardo:~/sources 507> cd ladr paul@leonardo:~/sources/ladr 508> ls total 312 -rw------- 1 paul staff 17987 May 19 13:16 COPYING -rw------- 1 paul staff 62287 May 19 13:16 Changelog -rw------- 1 paul staff 1492 May 19 13:16 Makefile -rw------- 1 paul staff 913 May 19 13:16 README.AMD_64 -rw------- 1 paul staff 162 May 19 13:16 README.first -rw------- 1 paul staff 610 May 19 13:16 README.make -rw------- 1 paul staff 290 May 19 13:16 README.release-reminder drwx------ 7 paul staff 238 May 19 13:16 TODO/ -rw------- 1 paul staff 78 May 19 13:16 VERSION_DATE.h drwx------ 22 paul staff 748 May 19 13:16 apps.examples/ drwx------ 56 paul staff 1904 May 19 13:16 apps.src/ drwx------ 7 paul staff 238 May 19 13:16 bob/ drwx------ 200 paul staff 6800 May 19 13:16 ladr/ -rw------- 1 paul staff 38551 May 19 13:16 libtoolize.patch drwx------ 5 paul staff 170 May 19 13:16 mace4.examples/ drwx------ 41 paul staff 1394 May 19 13:16 mace4.src/ drwx------ 4 paul staff 136 May 19 13:16 manpages/ drwx------ 6 paul staff 204 May 19 13:16 prover9.examples/ drwx------ 56 paul staff 1904 May 19 13:16 provers.src/ -rwx------ 1 paul staff 343 May 19 13:16 rev.py* -rw------- 1 paul staff 775 May 19 13:16 sed.gnu-blurb drwx------ 11 paul staff 374 May 19 13:16 test.src/ drwx------ 10 paul staff 340 May 19 13:16 utilities/ drwx------ 9 paul staff 306 May 19 13:16 utilities-old/ paul@leonardo:~/sources/ladr 509> git branch

master paul@leonardo:~/sources/ladr 510> git branch -a
master remotes/origin/HEAD -> origin/master remotes/origin/develop remotes/origin/ladr_to_tptp remotes/origin/makefile remotes/origin/master paul@leonardo:~/sources/ladr 511> git checkout --force makefile paul@leonardo:~/sources/ladr 512> gitk --all & [1] 5339 paul@leonardo:~/sources/ladr 513> git branch
master [1]+ Done gitk --all paul@leonardo:~/sources/ladr 514> git branch makefile paul@leonardo:~/sources/ladr 515> git branch makefile
master paul@leonardo:~/sources/ladr 516> git checkout --force makefile Switched to branch 'makefile' paul@leonardo:~/sources/ladr 517> git branch
makefile master paul@leonardo:~/sources/ladr 518> ls total 312 -rw------- 1 paul staff 17987 May 19 13:16 COPYING -rw------- 1 paul staff 62287 May 19 13:16 Changelog -rw------- 1 paul staff 1492 May 19 13:16 Makefile -rw------- 1 paul staff 913 May 19 13:16 README.AMD_64 -rw------- 1 paul staff 162 May 19 13:16 README.first -rw------- 1 paul staff 610 May 19 13:16 README.make -rw------- 1 paul staff 290 May 19 13:16 README.release-reminder drwx------ 7 paul staff 238 May 19 13:16 TODO/ -rw------- 1 paul staff 78 May 19 13:16 VERSION_DATE.h drwx------ 22 paul staff 748 May 19 13:16 apps.examples/ drwx------ 56 paul staff 1904 May 19 13:16 apps.src/ drwx------ 7 paul staff 238 May 19 13:16 bob/ drwx------ 200 paul staff 6800 May 19 13:16 ladr/ -rw------- 1 paul staff 38551 May 19 13:16 libtoolize.patch drwx------ 5 paul staff 170 May 19 13:16 mace4.examples/ drwx------ 41 paul staff 1394 May 19 13:16 mace4.src/ drwx------ 4 paul staff 136 May 19 13:16 manpages/ drwx------ 6 paul staff 204 May 19 13:16 prover9.examples/ drwx------ 56 paul staff 1904 May 19 13:16 provers.src/ -rwx------ 1 paul staff 343 May 19 13:16 rev.py -rw------- 1 paul staff 775 May 19 13:16 sed.gnu-blurb drwx------ 11 paul staff 374 May 19 13:16 test.src/ drwx------ 10 paul staff 340 May 19 13:16 utilities/ drwx------ 9 paul staff 306 May 19 13:16 utilities-old/ paul@leonardo:~/sources/ladr 519> make all cd ladr && make lib make libladr.a gcc -O -Wall -c -o order.o order.c gcc -O -Wall -c -o clock.o clock.c gcc -O -Wall -c -o nonport.o nonport.c gcc -O -Wall -c -o fatal.o fatal.c gcc -O -Wall -c -o ibuffer.o ibuffer.c gcc -O -Wall -c -o memory.o memory.c gcc -O -Wall -c -o hash.o hash.c gcc -O -Wall -c -o string.o string.c gcc -O -Wall -c -o strbuf.o strbuf.c gcc -O -Wall -c -o glist.o glist.c gcc -O -Wall -c -o options.o options.c gcc -O -Wall -c -o symbols.o symbols.c gcc -O -Wall -c -o avltree.o avltree.c avltree.c: In function ‘p_avl’: avltree.c:658: warning: cast from pointer to integer of different size gcc -O -Wall -c -o term.o term.c gcc -O -Wall -c -o termflag.o termflag.c gcc -O -Wall -c -o listterm.o listterm.c gcc -O -Wall -c -o tlist.o tlist.c gcc -O -Wall -c -o flatterm.o flatterm.c gcc -O -Wall -c -o multiset.o multiset.c gcc -O -Wall -c -o termorder.o termorder.c gcc -O -Wall -c -o parse.o parse.c gcc -O -Wall -c -o accanon.o accanon.c gcc -O -Wall -c -o unify.o unify.c gcc -O -Wall -c -o fpalist.o fpalist.c gcc -O -Wall -c -o fpa.o fpa.c gcc -O -Wall -c -o discrim.o discrim.c gcc -O -Wall -c -o discrimb.o discrimb.c gcc -O -Wall -c -o discrimw.o discrimw.c gcc -O -Wall -c -o dioph.o dioph.c gcc -O -Wall -c -o btu.o btu.c gcc -O -Wall -c -o btm.o btm.c gcc -O -Wall -c -o mindex.o mindex.c gcc -O -Wall -c -o basic.o basic.c gcc -O -Wall -c -o attrib.o attrib.c gcc -O -Wall -c -o formula.o formula.c gcc -O -Wall -c -o definitions.o definitions.c gcc -O -Wall -c -o literals.o literals.c gcc -O -Wall -c -o topform.o topform.c gcc -O -Wall -c -o clist.o clist.c gcc -O -Wall -c -o clauseid.o clauseid.c gcc -O -Wall -c -o clauses.o clauses.c gcc -O -Wall -c -o just.o just.c gcc -O -Wall -c -o cnf.o cnf.c gcc -O -Wall -c -o clausify.o clausify.c gcc -O -Wall -c -o parautil.o parautil.c gcc -O -Wall -c -o pindex.o pindex.c gcc -O -Wall -c -o compress.o compress.c gcc -O -Wall -c -o maximal.o maximal.c gcc -O -Wall -c -o lindex.o lindex.c gcc -O -Wall -c -o weight.o weight.c gcc -O -Wall -c -o weight2.o weight2.c gcc -O -Wall -c -o int_code.o int_code.c gcc -O -Wall -c -o features.o features.c gcc -O -Wall -c -o di_tree.o di_tree.c gcc -O -Wall -c -o fastparse.o fastparse.c fastparse.c: In function ‘fast_read_term’: fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:186: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments fastparse.c:187: warning: format not a string literal and no format arguments gcc -O -Wall -c -o random.o random.c gcc -O -Wall -c -o subsume.o subsume.c gcc -O -Wall -c -o clause_misc.o clause_misc.c gcc -O -Wall -c -o clause_eval.o clause_eval.c gcc -O -Wall -c -o complex.o complex.c gcc -O -Wall -c -o dollar.o dollar.c gcc -O -Wall -c -o flatdemod.o flatdemod.c gcc -O -Wall -c -o demod.o demod.c gcc -O -Wall -c -o clash.o clash.c gcc -O -Wall -c -o resolve.o resolve.c gcc -O -Wall -c -o paramod.o paramod.c gcc -O -Wall -c -o backdemod.o backdemod.c gcc -O -Wall -c -o hints.o hints.c gcc -O -Wall -c -o ac_redun.o ac_redun.c gcc -O -Wall -c -o xproofs.o xproofs.c gcc -O -Wall -c -o ivy.o ivy.c gcc -O -Wall -c -o interp.o interp.c gcc -O -Wall -c -o std_options.o std_options.c gcc -O -Wall -c -o banner.o banner.c gcc -O -Wall -c -o ioutil.o ioutil.c gcc -O -Wall -c -o tptp_trans.o tptp_trans.c gcc -O -Wall -c -o top_input.o top_input.c ar rs libladr.a order.o clock.o nonport.o fatal.o ibuffer.o memory.o hash.o string.o strbuf.o glist.o options.o symbols.o avltree.o term.o termflag.o listterm.o tlist.o flatterm.o multiset.o termorder.o parse.o accanon.o unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o dioph.o btu.o btm.o mindex.o basic.o attrib.o formula.o definitions.o literals.o topform.o clist.o clauseid.o clauses.o just.o cnf.o clausify.o parautil.o pindex.o compress.o maximal.o lindex.o weight.o weight2.o int_code.o features.o di_tree.o fastparse.o random.o subsume.o clause_misc.o clause_eval.o complex.o dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o backdemod.o hints.o ac_redun.o xproofs.o ivy.o interp.o std_options.o banner.o ioutil.o tptp_trans.o top_input.o ar: creating archive libladr.a cd mace4.src && make all cd ../ladr && make libladr.a make[2]: `libladr.a' is up to date. make clean /bin/rm -f .o make libmace4.a gcc -O -Wall -c -o estack.o estack.c gcc -O -Wall -c -o util.o util.c gcc -O -Wall -c -o print.o print.c print.c: In function ‘pmodel’: print.c:114: warning: format not a string literal and no format arguments print.c:114: warning: format not a string literal and no format arguments print.c:119: warning: format not a string literal and no format arguments print.c:119: warning: format not a string literal and no format arguments print.c:137: warning: format not a string literal and no format arguments print.c:137: warning: format not a string literal and no format arguments print.c:145: warning: format not a string literal and no format arguments print.c:145: warning: format not a string literal and no format arguments gcc -O -Wall -c -o syms.o syms.c gcc -O -Wall -c -o ground.o ground.c gcc -O -Wall -c -o arithmetic.o arithmetic.c gcc -O -Wall -c -o select.o select.c gcc -O -Wall -c -o propagate.o propagate.c gcc -O -Wall -c -o mstate.o mstate.c gcc -O -Wall -c -o negpropindex.o negpropindex.c gcc -O -Wall -c -o negprop.o negprop.c gcc -O -Wall -c -o ordercells.o ordercells.c gcc -O -Wall -c -o commandline.o commandline.c gcc -O -Wall -c -o msearch.o msearch.c ar rs libmace4.a estack.o util.o print.o syms.o ground.o arithmetic.o select.o propagate.o mstate.o negpropindex.o negprop.o ordercells.o commandline.o msearch.o ar: creating archive libmace4.a gcc -O -Wall -c -o mace4.o mace4.c gcc -O -Wall -o mace4 mace4.o libmace4.a ../ladr/libladr.a /bin/mv mace4 ../bin cd provers.src && make all cd ../ladr && make libladr make libladr.a make[3]:`libladr.a' is up to date. make clean /bin/rm -f .o cd ../mace4.src && make libmace4 make libmace4.a make[3]: `libmace4.a' is up to date. make clean /bin/rm -f .o gcc -O -Wall -c -o prover9.o prover9.c gcc -O -Wall -c -o index_lits.o index_lits.c gcc -O -Wall -c -o forward_subsume.o forward_subsume.c gcc -O -Wall -c -o demodulate.o demodulate.c gcc -O -Wall -c -o pred_elim.o pred_elim.c gcc -O -Wall -c -o unfold.o unfold.c gcc -O -Wall -c -o semantics.o semantics.c gcc -O -Wall -c -o giv_select.o giv_select.c gcc -O -Wall -c -o white_black.o white_black.c gcc -O -Wall -c -o actions.o actions.c gcc -O -Wall -c -o search.o search.c gcc -O -Wall -c -o utilities.o utilities.c gcc -O -Wall -c -o provers.o provers.c gcc -O -Wall -c -o foffer.o foffer.c gcc -O -Wall -lm -o prover9 prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o fof-prover9.o fof-prover9.c gcc -O -Wall -lm -o fof-prover9 fof-prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o autosketches4.o autosketches4.c gcc -O -Wall -lm -o autosketches4 autosketches4.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o newauto.o newauto.c gcc -O -Wall -lm -o newauto newauto.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o newsax.o newsax.c gcc -O -Wall -lm -o newsax newsax.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o ladr_to_tptp.o ladr_to_tptp.c ladr_to_tptp.c: In function ‘main’: ladr_to_tptp.c:46: warning: passing argument 2 of ‘std_prover_init_and_input’ from incompatible pointer type gcc -O -Wall -lm -o ladr_to_tptp ladr_to_tptp.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O -Wall -c -o tptp_to_ladr.o tptp_to_ladr.c gcc -O -Wall -lm -o tptp_to_ladr tptp_to_ladr.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a /bin/cp -p prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr ../bin usage: cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file target_file cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file ... target_directory make[1]: _* [install] Error 64 make: *\ [all] Error 2 paul@leonardo:~/sources/ladr 520> git show HEAD | head -n 1 commit eb622498737ab7695b278ee5bda5e354477f7f24 paul@leonardo:~/sources/ladr 521> git status

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

#

bin

nothing added to commit but untracked files present (use "git add" to track) paul@leonardo:~/sources/ladr 522> git log commit eb622498737ab7695b278ee5bda5e354477f7f24 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:27:07 2012 +0200

Read from the empty string, not NULL.

commit cdfc7ad6971fc8346a682040d723cbdf457e3398 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:26:47 2012 +0200

Only whitespace differences.

commit 248d353fd54aff362a728c06251a3bbb170e10c6 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:25:23 2012 +0200

Unnecessary whitespace.

commit ba258f00b2f12b3cb22f52b7842a38434ddebb12 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:24:05 2012 +0200

Stuff to ignore.

commit 03bbf3b4b2f4a87b542215166209c42000c872f7 Author: Jesse Alama jesse.alama@gmail.com Date: Fri May 4 10:15:52 2012 +0200

Initial commit (LADR 2009-11A)

paul@leonardo:~/sources/ladr 523> git branch

makefile master paul@leonardo:~/sources/ladr 524>

On May 19, 2012, at 3:43 AM, Jesse Alama wrote:

Can you please pull the latest commits in the makefile branch and try again? Commit 80e96f332dbe8815135a815fa903492d19c5f840 on my machine seems to work. One way to test all this is to kill everything in the ladr repo, except the .git directory, and then do
   git checkout --force makefile
and then
   make all
I don't trust that make clean kills everything.

Reply to this email directly or view it on GitHub: https://github.com/jessealama/ladr/issues/1#issuecomment-5800880

Hi Paul,

peoppenheimer reply@reply.github.com writes:

[snip]

/bin/cp -p prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr ../bin usage: cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file target_file cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file ... target_directory make[1]: * [install] Error 64 make: * [all] Error 2 paul@leonardo:~/sources/ladr 520> git show HEAD | head -n 1 commit eb622498737ab7695b278ee5bda5e354477f7f24 paul@leonardo:~/sources/ladr 521> git status

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

#

bin

nothing added to commit but untracked files present (use "git add" to track) paul@leonardo:~/sources/ladr 522> git log commit eb622498737ab7695b278ee5bda5e354477f7f24 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:27:07 2012 +0200
Read from the empty string, not NULL.

The failed call to cp is a red flag that something is really wrong here. From the git log I see that the commit you're using is from several days ago. The problem is that

$ git checkout --force makefile

isn't doing what we think it is. It is creating a new local branch called 'makefile' having nothing to do with the 'makefile' branch to which I've been pushing my commits. Try this (confirmed just now on my laptop with a totally fresh clone of the LADR repo):

$ git checkout -b makefile remotes/origin/makefile

This will create a new branch in your local repo called 'makefile' whose starting point is the latest commit on remotes/origin/makefile, i.e., the most recent commit that I pushed to GitHub on my 'makefile' branch. Sorry for the git trouble; I gave you bad advice. Can you please give this another try? Make sure that when you do git log after the checkout that you see, e.g., a commit message like this:

  commit 048a8dca1563025abc586ee1eb7ef2850d512bc1
  Author: Jesse Alama <jesse.alama@gmail.com>
  Date:   Sat May 19 12:56:55 2012 +0200

      Ignore the mace4 executable.

Jesse Alama http://centria.di.fct.unl.pt/~alama/

Dear Jesse,

That did it.

That also explains why switching branches in the github app did nothing, but now when I look at the project in the gitub app it shows that I'm on the makefile branch, and my local makefile branch is indeed starting from the remote makefile branch. The build of prover9 and mace4 produced correctly working versions, and your revised ladr_to_tptp seems to be working fine now, as witness the following transcript:

paul@leonardo:~/ComputationalPhilosophy/OntologicalArgument/1991/prover9 525> ~/sources/ladr/bin/ladr_to_tptp < unintended2.in > unintended2.p paul@leonardo:~/ComputationalPhilosophy/OntologicalArgument/1991/prover9 526> ls total 32 -rw-r--r--@ 1 paul staff 94 Feb 14 2011 unintended.txt -rw-r--r--@ 1 paul staff 422 Feb 14 2011 unintended1.in -rw-r--r--@ 1 paul staff 456 Feb 14 2011 unintended2.in -rw------- 1 paul staff 811 May 20 12:58 unintended2.p paul@leonardo:~/ComputationalPhilosophy/OntologicalArgument/1991/prover9 527> cat unintended2.p

% The LADR formulas contain function or predicate symbols % that are not legal TPTP symbols, and we have replaced those % symbols with new symbols. Here is the list of the unaccepted % symbols and the corresponding replacements. % % (arity 2) Ex1 tptp0 % (arity 1) Object tptp1 % (arity 1) Relation1 tptp2 % (arity 2) Is_the tptp3

fof(sos,axiom,! [X0] : ! [X1] : ! [X2] : ((tptp2(X0) & (tptp2(X1) & tptp1(X2))) => ((tptp3(X2,X0) & tptp0(X1,X2)) <=> ? [X3] : (tptp1(X3) & (tptp0(X0,X3) & (! [X4] : (tptp1(X4) => (tptp0(X0,X4) => X4 = X3)) & tptp0(X1,X3))))))). fof(goals,conjecture,! [X5] : ! [X6] : ((tptp2(X5) & tptp2(X6)) => (? [X7] : (tptp1(X7) & (tptp0(X5,X7) & (! [X8] : (tptp1(X8) => (tptp0(X5,X8) => X8 = X7)) & tptp0(X6,X7)))) => ! [X9] : (tptp1(X9) => tptp0(X6,X9))))). paul@leonardo:~/ComputationalPhilosophy/OntologicalArgument/1991/prover9 528>

Thank you for all your help!

Best, Paul

On May 20, 2012, at 3:12 AM, Jesse Alama wrote:

Hi Paul,

peoppenheimer reply@reply.github.com writes:

[snip]

/bin/cp -p prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr ../bin usage: cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file target_file cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file ... target_directory make[1]: * [install] Error 64 make: * [all] Error 2 paul@leonardo:~/sources/ladr 520> git show HEAD | head -n 1 commit eb622498737ab7695b278ee5bda5e354477f7f24 paul@leonardo:~/sources/ladr 521> git status

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

#

bin

nothing added to commit but untracked files present (use "git add" to track) paul@leonardo:~/sources/ladr 522> git log commit eb622498737ab7695b278ee5bda5e354477f7f24 Author: Jesse Alama jesse.alama@gmail.com Date: Wed May 16 02:27:07 2012 +0200

Read from the empty string, not NULL.

The failed call to cp is a red flag that something is really wrong here. From the git log I see that the commit you're using is from several days ago. The problem is that

$ git checkout --force makefile

isn't doing what we think it is. It is creating a new local branch called 'makefile' having nothing to do with the 'makefile' branch to which I've been pushing my commits. Try this (confirmed just now on my laptop with a totally fresh clone of the LADR repo):

$ git checkout -b makefile remotes/origin/makefile

This will create a new branch in your local repo called 'makefile' whose starting point is the latest commit on remotes/origin/makefile, i.e., the most recent commit that I pushed to GitHub on my 'makefile' branch. Sorry for the git trouble; I gave you bad advice. Can you please give this another try? Make sure that when you do git log after the checkout that you see, e.g., a commit message like this:
 commit 048a8dca1563025abc586ee1eb7ef2850d512bc1
 Author: Jesse Alama <jesse.alama@gmail.com>
 Date:   Sat May 19 12:56:55 2012 +0200

     Ignore the mace4 executable.
Jesse Alama http://centria.di.fct.unl.pt/~alama/

Reply to this email directly or view it on GitHub: https://github.com/jessealama/ladr/issues/1#issuecomment-5807806

jessealama / ladr

No rule to make target `libladr.a'. #1

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

bin

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

bin

On branch makefile

Untracked files:

(use "git add ..." to include in what will be committed)

bin