| author | schirmer <schirmer@in.tum.de> |
| Sun, 15 Nov 2009 13:06:07 +0100 | |
| changeset 33693 | 9d76c8080aea |
| permissions | -rw-r--r-- |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
1 |
# |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
2 |
# $Id$ |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
3 |
# |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
5 |
## targets |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
7 |
default: HOL-record |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
8 |
images: |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
9 |
test: HOL-record |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
10 |
all: images test |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
13 |
## global settings |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
15 |
SRC = $(ISABELLE_HOME)/src |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
16 |
OUT = $(ISABELLE_OUTPUT) |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
17 |
LOG = $(OUT)/log |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
19 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
20 |
## HOL-record |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
22 |
HOL: |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
23 |
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
24 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
25 |
HOL-record: HOL $(LOG)/HOL-record.gz |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
26 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
27 |
$(LOG)/HOL-record.gz: RecordBenchmark.thy |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
28 |
@cd ..; $(ISABELLE_TOOL) usedir -s HOL-record $(OUT)/HOL HOL-record |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
29 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
30 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
31 |
## clean |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
32 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
33 |
clean: |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
34 |
@rm -f $(LOG)/HOL-record.gz |