Admin/Benchmarks/IsaMakefile
author schirmer <schirmer@in.tum.de>
Sun, 15 Nov 2009 13:06:07 +0100
changeset 33693 9d76c8080aea
parent 28500 4b79e5d3d0aa
child 33696 2c7c79ca6c23
permissions -rw-r--r--
added benchmark for large records
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     1
#
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     2
# $Id$
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     3
#
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     4
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     5
## targets
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     6
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     7
default: HOL-datatype
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     8
images:
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
     9
test: HOL-datatype HOL-record
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    10
all: images test
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    11
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    12
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    13
## global settings
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    14
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    15
SRC = $(ISABELLE_HOME)/src
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    16
OUT = $(ISABELLE_OUTPUT)
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    17
LOG = $(OUT)/log
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    18
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    19
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    20
## HOL-datatype
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    21
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    22
HOL:
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 10099
diff changeset
    23
	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    24
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    25
HOL-datatype: HOL $(LOG)/HOL-datatype.gz
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    26
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    27
$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/Brackin.thy \
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    28
  HOL-datatype/Instructions.thy HOL-datatype/SML.thy \
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    29
  HOL-datatype/Verilog.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 10099
diff changeset
    30
	@$(ISABELLE_TOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    31
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    32
HOL-record: HOL $(LOG)/HOL-record.gz
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    33
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    34
$(LOG)/HOL-record.gz: HOL-record/RecordBenchmark.thy 
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    35
	@$(ISABELLE_TOOL) usedir -s HOL-record $(OUT)/HOL HOL-record
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    36
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    37
## clean
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    38
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    39
clean:
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    40
	@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz