IsaMakefile
author urbanc
Thu, 25 Nov 2010 18:54:45 +0000
changeset 24 f72c82bf59e5
parent 16 663816814e3e
child 30 f5db9e08effc
permissions -rw-r--r--
added paper
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
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    22
	@$(USEDIR) -D generated -f ROOT.ML HOL Slides
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
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    32
session2: Paper/ROOT.ML \
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    33
         Paper/document/root* \
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    34
         Paper/Paper.thy
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    35
	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    36
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    37
paper: session2 
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    38
	rm -f Paper/generated/*.aux # otherwise latex will fall over
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    39
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    40
	cp Paper/generated/root.pdf Paper/paper.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/*
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    47
	rm -rf Paper/generated/*