Mercurial Mercurial > hg > regexp / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IsaMakefile
author urbanc
Sun, 20 Nov 2011 22:53:50 +0000
changeset 258 1abf8586ee6b
parent 203 5d724fe0e096
child 333 813e7257c7c3
permissions -rw-r--r--
added slides for a talk in St Andrews


## targets

default: paper
all: slides paper

## global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log


USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 


## Slides

session1: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL Slides

slides: session1 
	rm -f Slides/generated/*.aux # otherwise latex will fall over
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
	cp Slides/generated/root.beamer.pdf Slides/slides.pdf     

## Slides 1

session11: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides1.thy
	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides

slides1: session11 
	rm -f Slides/generated/*.aux # otherwise latex will fall over
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
	cp Slides/generated/root.beamer.pdf Slides/slides1.pdf   

## Slides 2

session22: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides2.thy
	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides

slides2: session22 
	rm -f Slides/generated/*.aux # otherwise latex will fall over
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf   

## long paper

session2: tphols-2011/ROOT.ML \
         tphols-2011/document/root* \
         *.thy
	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 

paper: session2 
	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf     

## full paper

fullsession2: tphols-2011/ROOT.ML \
         tphols-2011/document/root* \
         *.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011 

fullpaper: fullsession2 
	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf   



## ITP paper

session3: Paper/ROOT.ML \
	Paper/document/root* \
	Paper/*.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL Paper

itp: session3
	rm -f Paper/generated/*.aux # otherwise latex will fall over      
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cd Paper/generated ; bibtex root
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
	cp Paper/generated/root.pdf paper.pdf     

## Journal Version

session4: Journal/ROOT.ML \
	Journal/document/root* \
	Journal/*.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL Journal

journal: session4
	rm -f Journal/generated/*.aux # otherwise latex will fall over       
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cd Journal/generated ; bibtex root
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
	cp Journal/generated/root.pdf journal.pdf     


## clean

clean:
	rm -rf Slides/generated/*
	rm -rf tphols-2011/generated/*
regexp