IsaMakefile
author zhang
Mon, 24 Jan 2011 11:29:55 +0000
changeset 30 f5db9e08effc
parent 24 f72c82bf59e5
child 31 b6815473ee2e
permissions -rw-r--r--
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     1
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     2
## targets
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     3
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
     4
default: paper
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
     5
all: slides paper
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     6
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     7
## global settings
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     8
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     9
SRC = $(ISABELLE_HOME)/src
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    10
OUT = $(ISABELLE_OUTPUT)
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    11
LOG = $(OUT)/log
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    12
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    13
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    14
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    15
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    16
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    17
## Slides
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    18
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    19
session1: Slides/ROOT.ML \
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    20
         Slides/document/root* \
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    21
         Slides/Slides.thy
30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    22
	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    23
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    24
slides: session1 
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    25
	rm -f Slides/generated/*.aux # otherwise latex will fall over
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    26
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    27
	cp Slides/generated/root.beamer.pdf Slides/slides.pdf     
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    28
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    29
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    30
## Paper
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    31
30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    32
session2: tphols-2011/ROOT.ML \
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    33
         tphols-2011/document/root* \
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    34
         ../*.thy
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    35
	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    36
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    37
paper: session2 
30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    38
	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    39
	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    40
	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf     
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    41
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    42
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    43
## clean
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    44
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    45
clean:
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    46
	rm -rf Slides/generated/*
30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents: 24
diff changeset
    47
	rm -rf tphols-2011/generated/*