No rule to make target `libladr.a'.

[peoppenheimer]

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 VERSION_DATE.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_to_ladr
  /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 top_input.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>

[jessealama]

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.

[peoppenheimer]

Pulled the branch using the github app. 7353295 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_to_ladr
/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 top_input.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:
#1 (comment)

[jessealama]

Can you please pull the latest commits in the makefile branch and try again? Commit 80e96f3 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.

[peoppenheimer]

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 ‘p_model’: 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 eb62249
  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 eb62249
  Author: Jesse Alama jesse.alama@gmail.com
  Date: Wed May 16 02:27:07 2012 +0200

  Read from the empty string, not NULL.

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

Only whitespace differences.

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

Unnecessary whitespace.

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

Stuff to ignore.

commit 03bbf3b
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 80e96f3 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:
#1 (comment)

[jessealama]

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 eb62249
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 eb62249
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/

[peoppenheimer]

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 eb62249
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 eb62249
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:
#1 (comment)