IsaMakefile
author Christian Urban <urbanc@in.tum.de>
Wed, 16 Dec 2009 14:26:14 +0100
changeset 756 27eb796ad842
parent 754 b85875d65b10
child 757 c129354f2ff6
permissions -rw-r--r--
first fix
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
597
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
## targets
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
default: Quot
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
images: 
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
601
81f40b8bde7b added "end" to each example theory
Christian Urban <urbanc@in.tum.de>
parents: 597
diff changeset
     7
all: Quot
597
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
## global settings
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
SRC = $(ISABELLE_HOME)/src
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
OUT = $(ISABELLE_OUTPUT)
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
LOG = $(OUT)/log
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    16
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -D generated
597
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
## Quot
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
Quot: $(LOG)/HOL-Quot.gz
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
$(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
756
27eb796ad842 first fix
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    23
	@$(USEDIR) HOL-Nominal Quot
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    24
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    25
paper: $(LOG)/HOL-Quot-Paper.gz
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    26
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    27
$(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    28
	@$(USEDIR) HOL Paper
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    29
	$(ISATOOL) document -o pdf  Paper/generated
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents: 604
diff changeset
    30
	@cp Paper/document.pdf paper.pdf
597
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
## clean
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
clean:
8a1c8dc72b5c directory re-arrangement
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
	@rm -f $(LOG)/HOL-Quot.gz