diff -r 78d828f43cdf -r 4b4742aa43f2 IsaMakefile --- a/IsaMakefile Sat Dec 17 16:58:11 2011 +0000 +++ b/IsaMakefile Sat Dec 17 17:03:01 2011 +0000 @@ -4,7 +4,7 @@ default: tests images: -all: tests esop pearl pearl-jv qpaper slides +all: tests ## global settings @@ -23,156 +23,6 @@ $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy @cd Nominal; $(USEDIR) -b -d "" HOL Nominal2 -## ESOP Paper - -esop: $(LOG)/HOL-ESOP-Paper.gz - -$(LOG)/HOL-ESOP-Paper.gz: ESOP-Paper/ROOT.ML ESOP-Paper/document/root.* ESOP-Paper/*.thy - @$(USEDIR) -f ROOT.ML -D generated Nominal2 ESOP-Paper - $(ISABELLE_TOOL) document -o pdf ESOP-Paper/generated - @cp ESOP-Paper/document.pdf esop-paper.pdf - -## LMCS Paper - -lmcs: $(LOG)/HOL-LMCS-Paper.gz - -$(LOG)/HOL-LMCS-Paper.gz: LMCS-Paper/ROOT.ML LMCS-Paper/document/root.* LMCS-Paper/*.thy - @$(USEDIR) -f ROOT.ML -D generated Nominal2 LMCS-Paper - $(ISABELLE_TOOL) document -o pdf LMCS-Paper/generated - @cp LMCS-Paper/document.pdf lmcs-paper.pdf - -## Pearl Paper ITP - -pearl: $(LOG)/HOL-Pearl.gz - -$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy - @$(USEDIR) -D generated HOL Pearl - $(ISABELLE_TOOL) document -o pdf Pearl/generated - @cp Pearl/document.pdf pearl.pdf - -## Pearl Journal Paper - -$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Nominal/*.thy - @cd Pearl-jv; $(USEDIR) -b -f ROOT.ML HOL HOL-Pearl-jv - -pearl-jv: $(LOG)/HOL-Pearl-jv.gz Pearl-jv/ROOT2.ML Pearl-jv/document/root.* Pearl-jv/*.thy - @$(USEDIR) -f ROOT2.ML -D generated HOL-Pearl-jv Pearl-jv - @$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated - @cp Pearl-jv/document.pdf pearl-jv.pdf - -## Quotient Paper - -qpaper: $(LOG)/HOL-QPaper.gz - -$(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy - @$(USEDIR) -D generated HOL Quotient-Paper - $(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated - @cp Quotient-Paper/document.pdf qpaper.pdf - -## Nominal Functions paper - -fnpaper: $(LOG)/HOL-FnPaper.gz - -$(LOG)/HOL-FnPaper.gz: Fun-Paper/ROOT.ML Fun-Paper/document/root.* Fun-Paper/*.thy - @$(USEDIR) -D generated HOL Fun-Paper - $(ISABELLE_TOOL) document -o pdf Fun-Paper/generated - @cp Fun-Paper/document.pdf fnpaper.pdf - -## Slides - -session1: Slides/ROOT1.ML \ - Slides/document/root* \ - Slides/Slides1.thy - @$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides - -slides1: session1 - rm -f Slides/generated1/*.aux # otherwise latex will fall over - cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf - -session2: Slides/ROOT2.ML \ - Slides/document/root* \ - Slides/Slides2.thy - @$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides - -slides2: session2 - rm -f Slides/generated2/*.aux # otherwise latex will fall over - cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf - -session3: Slides/ROOT3.ML \ - Slides/document/root* \ - Slides/Slides3.thy - @$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides - -slides3: session3 - rm -f Slides/generated3/*.aux # otherwise latex will fall over - cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf - -session4: Slides/ROOT4.ML \ - Slides/document/root* \ - Slides/Slides4.thy - @$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides - -slides4: session4 - rm -f Slides/generated4/*.aux # otherwise latex will fall over - cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf - -session5: Slides/ROOT5.ML \ - Slides/document/root* \ - Slides/Slides5.thy - @$(USEDIR) -D generated5 -f ROOT5.ML HOL-Nominal Slides - -slides5: session5 - rm -f Slides/generated5/*.aux # otherwise latex will fall over - cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf - -session6: Slides/ROOT6.ML \ - Slides/document/root* \ - Slides/Slides6.thy - @$(USEDIR) -D generated6 -f ROOT6.ML HOL-Nominal Slides - -slides6: session6 - rm -f Slides/generated6/*.aux # otherwise latex will fall over - cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf - -session7: Slides/ROOT7.ML \ - Slides/document/root* \ - Slides/Slides6.thy - @$(USEDIR) -D generated7 -f ROOT7.ML HOL Slides - -slides7: session7 - rm -f Slides/generated7/*.aux # otherwise latex will fall over - cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf - -session8: Slides/ROOT8.ML \ - Slides/document/root* \ - Slides/Slides6.thy - @$(USEDIR) -D generated8 -f ROOT8.ML HOL-Nominal Slides - -slides8: session8 - rm -f Slides/generated8/*.aux # otherwise latex will fall over - cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf - -slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 - - - - ## clean clean: