diff -r b32b3bd99150 -r 6b26b1fd4da5 IsaMakefile --- a/IsaMakefile Thu Sep 21 14:15:55 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ - -## targets - -default: itp -all: session itp slides1 - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -USEDIR = $(ISABELLE_TOOL) usedir -v true -t true - - -## Slides - -session1: Slides/ROOT1.ML \ - Slides/document/root* \ - Slides/Slides1.thy - @$(USEDIR) -D generated -f ROOT1.ML HOL Slides - -slides1: 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 slides1.pdf - -## Slides - -session2: Slides/ROOT2.ML \ - Slides/document/root* \ - Slides/Slides2.thy - @$(USEDIR) -D generated -f ROOT2.ML HOL Slides - -slides2: session2 - 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 slides2.pdf - - -# main files - -session: ./ROOT.ML ./*.thy - @$(USEDIR) -b -D generated -f ROOT.ML HOL Prio - - -# itp paper - -itp: Paper/*.thy Paper/*.ML - @$(USEDIR) -D generated -f ROOT.ML Prio Paper - 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 - -# C&L paper - -jour: Journal/*.thy Journal/*.ML - @$(USEDIR) -D generated -f ROOT.ML Prio Journal - 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 - - -