prio/IsaMakefile
changeset 360 66e0ec8acedc
parent 282 a3b4eed091d2
child 361 484c7b83f251
equal deleted inserted replaced
359:1b9163229f3f 360:66e0ec8acedc
     1 
     1 
     2 ## targets
     2 ## targets
     3 
     3 
     4 default: itp
     4 default: itp
     5 all: session itp
     5 all: session itp slides1
     6 
     6 
     7 ## global settings
     7 ## global settings
     8 
     8 
     9 SRC = $(ISABELLE_HOME)/src
     9 SRC = $(ISABELLE_HOME)/src
    10 OUT = $(ISABELLE_OUTPUT)
    10 OUT = $(ISABELLE_OUTPUT)
    14 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
    14 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
    15 
    15 
    16 
    16 
    17 ## Slides
    17 ## Slides
    18 
    18 
       
    19 session1: Slides/ROOT1.ML \
       
    20 	Slides/document/root* \
       
    21 	Slides/Slides1.thy
       
    22 	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
       
    23 
       
    24 slides1: session1
       
    25 	rm -f Slides/generated/*.aux # otherwise latex will fall over
       
    26 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
       
    27 	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
       
    28 
       
    29 # main files                        
       
    30 
    19 session: ./ROOT.ML ./*.thy
    31 session: ./ROOT.ML ./*.thy
    20 	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
    32 	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
       
    33 
       
    34 
       
    35 # itp paper
    21 
    36 
    22 itp: Paper/*.thy Paper/*.ML 
    37 itp: Paper/*.thy Paper/*.ML 
    23 	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
    38 	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
    24 	rm -f Paper/generated/*.aux # otherwise latex will fall over  
    39 	rm -f Paper/generated/*.aux # otherwise latex will fall over  
    25 	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
    40 	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex