Changeset 179 for trunk/backmath

Show
Ignore:
Timestamp:
01/04/08 16:36:23 (1 year ago)
Author:
BCS
Message:

Darn stupid merge saved the wrong file!!!!

Files:

Legend:

Unmodified
Added
Removed
Modified
Copied
Moved

  • trunk/backmath/makefile.linux

    r178 r179  
    1 ACL2=../acl2/acl2-sources/saved_acl2 
    21CL=gcl 
    3 NOPROOFP=false 
    4  
    5 ifeq ($(NOPROOFP),false) 
    6     CERT=lemma.cert 
    7 else 
    8     CERT= 
    9 endif 
    102 
    113all : backmath 
    …… 
    135    echo -n total rules generated:; grep alias generated_rules.d | wc -l 
    146 
    15 play : 
    16     $(ACL2) < play.lisp 
    17  
    187tooling : 
    198    $(CL) < do.lisp 
    209 
    21 proven : tests all 
    22  
    2310clean : 
    2411    rm -f \ 
    25     cert_*_log.txt \ 
    26     thm_gen_log.txt \ 
    27     test_lisp_output.lisp \ 
    28     proof_file.txt proof_file_.txt \ 
    2912    gen_log.txt \ 
    3013    backmath backmath.o generated_rules.d \ 
    31     not *.bak tests 
    32  
    33 clean_cert : 
    34     rm -f *.o *.cert  
    3514 
    3615backmath : backmath.o 
    …… 
    4120    dmd -c backmath.d -J. 
    4221 
    43 generated_rules.d : gen_code_for_template.lisp generate_case.lisp meta.lisp rule_sorting.lisp string_stuff.lisp tests 
     22generated_rules.d : gen_code_for_template.lisp generate_case.lisp meta.lisp rule_sorting.lisp string_stuff.lisp 
    4423    true ========= Generate Lib 
    4524    $(CL) < gen_code_for_template.lisp > gen_log.txt 
    4625    grep CODE_GEN_DONE gen_log.txt 
    4726 
    48 tests : proof_file_.txt 
    49     touch tests 
    50  
    51 proof_file_.txt : not test_lisp_output.lisp $(CERTP) 
    52     true ========= Test ruleset 
    53     $(NOPROOFP) || $(ACL2) > proof_file.txt < test_lisp_output.lisp 
    54     $(NOPROOFP) || (\ 
    55         echo failed ; grep FAILED proof_file.txt | wc -l ;\ 
    56         echo errored ; grep "HARD ACL2 ERROR" proof_file.txt | wc -l ;\ 
    57         echo passed ; grep "Q.E.D." proof_file.txt | wc -l ;\ 
    58         echo total ; grep THM test_lisp_output.lisp | wc -l ;\ 
    59         (\ 
    60             grep THM test_lisp_output.lisp | wc -l ;\ 
    61             grep FAILED proof_file.txt | wc -l ;\ 
    62             echo 100*r/nq \ 
    63         ) | dc ;\ 
    64         echo % failed \ 
    65         ) 
    66     $(NOPROOFP) || ./not grep -e FAILED -e "HARD ACL2 ERROR" proof_file.txt > /dev/null 
    67     $(NOPROOFP) && touch proof_file_.txt 
    68     if [ -e proof_file.txt ]; then cp proof_file.txt proof_file_.txt; fi 
    69  
    70 test_lisp_output.lisp : math.lisp meta.lisp 
    71     true ========= Generate tests 
    72     $(CL) < math.lisp > thm_gen_log.txt 
    73     sed -e "s/#://g" -e "s/#(//" -e "s/)#//" test_lisp_output.lisp | \ 
    74         sed "s/(THM/(cw __LINE__)(THM/" | \ 
    75         cpp | \ 
    76         grep -v "^#" | \ 
    77         sed 's/(cw \([0-9]*\))/(CW "\1")/' > tmp 
    78     mv tmp test_lisp_output.lisp 
    79     wc -l test_lisp_output.lisp 
    80  
    81 book : lemma2.cert 
    82      
    83 #lemma.cert : lemma.lisp do_cert.lisp not 
    84 #   true ========= certify my lemma book 
    85 #   $(ACL2) < do_cert.lisp > cert_log.txt 
    86 #   grep lemma.lisp cert_log.txt | grep -v -e Step -e ATTEMPT 
    87 #   ./not grep FAILED cert_log.txt 
    88  
    89 lemma2.cert : lemma_arth-2-meta.cert lemma_arth-with-meta.cert 
    90  
    91 %.cert : %.lisp do_%.lisp not 
    92     true ========= certify my $* book 
    93     $(ACL2) < do_$*.lisp > cert_$*_log.txt 
    94     grep $*.lisp cert_$*_log.txt | grep -v -e Step -e ATTEMPT 
    95     ./not grep FAILED cert_$*_log.txt 
    96  
    97 #   cp $*.cert $*.cert2 
    98  
    99 do_%.lisp : 
    100     (\ 
    101     echo -n '(defpkg "BM_' ;\ 
    102     echo $* | awk '{a=toupper($$0); printf a};end' - ;\ 
    103     echo '"' ;\ 
    104     echo '   (union-eq' ;\ 
    105     echo '     *common-lisp-symbols-from-main-lisp-package*' ;\ 
    106     echo '     *acl2-exports*' ;\ 
    107     echo '   )' ;\ 
    108     echo ')' ;\ 
    109     echo -n '(certify-book "' ;\ 
    110     echo -n $* ;\ 
    111     echo '" 1 t)' ;\ 
    112     ) > $@ 
    113  
    114  
    115      
    116  
    117 not : not.c 
    118     true ========= build NOT utill 
    119     gcc not.c -o not