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;
wenzelm@2491
     1
#
wenzelm@2491
     2
# IsaMakefile for CTT
wenzelm@2491
     3
#
wenzelm@2491
     4
wenzelm@4518
     5
## targets
wenzelm@4518
     6
wenzelm@4518
     7
default: CTT
wenzelm@4518
     8
images: CTT
wenzelm@4518
     9
test: CTT-ex
wenzelm@4518
    10
all: images test
wenzelm@4518
    11
wenzelm@4518
    12
wenzelm@4518
    13
## global settings
wenzelm@4518
    14
wenzelm@4518
    15
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    16
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    17
LOG = $(OUT)/log
wenzelm@2491
    18
wenzelm@4518
    19
wenzelm@4518
    20
## CTT
wenzelm@4518
    21
wenzelm@4518
    22
CTT: Pure $(OUT)/CTT
wenzelm@2491
    23
wenzelm@4518
    24
Pure:
wenzelm@28500
    25
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
wenzelm@2491
    26
wenzelm@19761
    27
$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
wenzelm@19761
    28
  Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
wenzelm@28500
    29
	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
wenzelm@2491
    30
wenzelm@4518
    31
wenzelm@4518
    32
## CTT-ex
wenzelm@2491
    33
wenzelm@4518
    34
CTT-ex: CTT $(LOG)/CTT-ex.gz
wenzelm@4518
    35
wenzelm@19761
    36
$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
wenzelm@19761
    37
  ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
wenzelm@28500
    38
	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
wenzelm@2491
    39
wenzelm@4518
    40
wenzelm@4518
    41
## clean
wenzelm@4447
    42
wenzelm@4447
    43
clean:
wenzelm@4518
    44
	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz