diff -r a6f3e1b08494 -r b6873d123f9b IsaMakefile --- a/IsaMakefile Sat May 12 21:05:59 2012 +0100 +++ b/IsaMakefile Sat May 12 21:39:09 2012 +0100 @@ -1,10 +1,10 @@ ## targets -default: session +default: tests images: -all: tests esop pearl pearl-jv qpaper qpaper-jv slides lmcs +all: tests ## global settings @@ -13,204 +13,15 @@ OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -m no_brackets - -## Nominal2 - -session: $(LOG)/HOL-Nominal2.gz - -$(LOG)/HOL-Nominal2.gz: Nominal/FROOT.ML Nominal/*.thy - @cd Nominal; $(USEDIR) -f FROOT.ML -b -d "" HOL Nominal2 +USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -m no_brackets ##-D generated -## tests - -tests: $(LOG)/HOL-Nominal2-tests.gz - -$(LOG)/HOL-Nominal2-tests.gz: Nominal/ROOT.ML Nominal/*.thy - @$(USEDIR) HOL Nominal - @$(USEDIR) HOL Tutorial - -## 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 - -## Quotient Journal Paper - -qpaper-jv: $(LOG)/HOL-QPaper-jv.gz - -$(LOG)/HOL-QPaper-jv.gz: Quotient-Paper-jv/ROOT.ML Quotient-Paper-jv/document/root.* Quotient-Paper-jv/*.thy - @$(USEDIR) -D generated HOL Quotient-Paper-jv - $(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated - @cp Quotient-Paper-jv/document.pdf qpaper-jv.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 +## Nominal2 -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 +tests: $(LOG)/HOL-Nominal2.gz -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 - -session9: Slides/ROOT9.ML \ - Slides/document/root* \ - Slides/Slides6.thy - @$(USEDIR) -D generated9 -f ROOT9.ML HOL-Nominal Slides - -slides9: session9 - rm -f Slides/generated9/*.aux # otherwise latex will fall over - cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf - -sessionA: Slides/ROOTA.ML \ - Slides/document/root* \ - Slides/SlidesA.thy - @$(USEDIR) -D generatedA -f ROOTA.ML HOL-Nominal Slides - -slidesA: sessionA - rm -f Slides/generatedA/*.aux # otherwise latex will fall over - cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generatedA/root.beamer.pdf Slides/slidesA.pdf - -slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9 slidesA - - - +$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy + @cd Nominal; $(USEDIR) -b -d "" HOL Nominal2 ## clean