nominal2: IsaMakefile@07ffa4e41659 (annotated)

1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	## targets
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2351 diff changeset	4	default: test
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	images:
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	7	all: tests paper pearl pearl-jv qpaper
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	## global settings
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	11
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	SRC = $(ISABELLE_HOME)/src
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	OUT = $(ISABELLE_OUTPUT)
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	LOG = $(OUT)/log
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ##-D generated
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	## Nominal2
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	21	tests: $(LOG)/HOL-Nominal2.gz
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
1491 f970ca9b5bec paper uses now a heap file - does not compile so long anymore Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	24	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	26	## Nominal2 Paper
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	27
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	paper: $(LOG)/HOL-Nominal2-Paper.gz
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
1775 86122d793f32 typos in paper Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	30	$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
1491 f970ca9b5bec paper uses now a heap file - does not compile so long anymore Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	31	@$(USEDIR) -D generated Nominal Paper
1484 dc7b049d9072 made paper to compile Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	32	$(ISABELLE_TOOL) document -o pdf Paper/generated
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	@cp Paper/document.pdf paper.pdf
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	35	## Pearl Paper ITP
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	36
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	37	pearl: $(LOG)/HOL-Pearl.gz
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	38
1775 86122d793f32 typos in paper Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	39	$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	40	@$(USEDIR) -D generated HOL Pearl
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	41	$(ISABELLE_TOOL) document -o pdf Pearl/generated
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	42	@cp Pearl/document.pdf pearl.pdf
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	43
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	44	## Pearl Journal Paper
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	45
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	46	pearl-jv: $(LOG)/HOL-Pearl-jv.gz
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	47
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	48	$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Pearl-jv/document/root.* Pearl-jv/*.thy
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	49	@$(USEDIR) -D generated HOL Pearl-jv
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	50	$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	51	@cp Pearl-jv/document.pdf pearl-jv.pdf
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	52
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	53
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	54	## Quotient Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	55
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	56	qpaper: $(LOG)/HOL-QPaper.gz
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	57
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	58	$(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	59	@$(USEDIR) -D generated HOL Quotient-Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	60	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	61	@cp Quotient-Paper/document.pdf qpaper.pdf
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	62
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	63	## Slides
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	64
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	65	session1: Slides/ROOT1.ML \
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	66	Slides/document/root* \
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	67	Slides/Slides1.thy
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	68	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	69
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	70	slides1: session1
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	71	rm -f Slides/generated1/*.aux # otherwise latex will fall over
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	72	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	73	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	74	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	75
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	76	session2: Slides/ROOT2.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	77	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	78	Slides/Slides2.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	79	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	80
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	81	slides2: session2
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	82	rm -f Slides/generated2/*.aux # otherwise latex will fall over
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	83	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	84	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	85	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	86
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	87	session3: Slides/ROOT3.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	88	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	89	Slides/Slides3.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	90	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	91
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	92	slides3: session3
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	93	rm -f Slides/generated3/*.aux # otherwise latex will fall over
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	94	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	95	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	96	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	97
2459 ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	98	session4: Slides/ROOT4.ML \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	99	Slides/document/root* \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	100	Slides/Slides4.thy
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	101	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	102
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	103	slides4: session4
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	104	rm -f Slides/generated4/*.aux # otherwise latex will fall over
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	105	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	106	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	107	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	108
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	109	slides: slides4
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	110
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	111
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	112
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	113
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	## clean
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	115
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	clean:
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	117	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz

author	Christian Urban <urbanc@in.tum.de>
	Fri, 03 Sep 2010 22:35:35 +0800
changeset 2465	07ffa4e41659
parent 2459	ac3470e1e5af
child 2479	a9b6a00b1ba0
permissions	-rw-r--r--