src/CTT/IsaMakefile
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 36862 952b2b102a0a
child 42138 e54a985daa61
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 #
     2 # IsaMakefile for CTT
     3 #
     4 
     5 ## targets
     6 
     7 default: CTT
     8 images: CTT
     9 test: CTT-ex
    10 all: images test
    11 
    12 
    13 ## global settings
    14 
    15 SRC = $(ISABELLE_HOME)/src
    16 OUT = $(ISABELLE_OUTPUT)
    17 LOG = $(OUT)/log
    18 
    19 
    20 ## CTT
    21 
    22 CTT: Pure $(OUT)/CTT
    23 
    24 Pure:
    25 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    26 
    27 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
    28   Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
    29 	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
    30 
    31 
    32 ## CTT-ex
    33 
    34 CTT-ex: CTT $(LOG)/CTT-ex.gz
    35 
    36 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
    37   ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
    38 	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
    39 
    40 
    41 ## clean
    42 
    43 clean:
    44 	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz