Admin/Benchmarks/IsaMakefile
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 33696 2c7c79ca6c23
child 44640 3e666dcdcd32
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
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
## targets
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     3
33696
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
     4
default: all
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     5
images:
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
     6
test: HOL-datatype HOL-record
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     7
all: images test
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     8
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
     9
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    10
## global settings
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    11
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    12
SRC = $(ISABELLE_HOME)/src
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    13
OUT = $(ISABELLE_OUTPUT)
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    14
LOG = $(OUT)/log
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    15
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    16
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    17
## HOL-datatype
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    18
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    19
HOL:
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 10099
diff changeset
    20
	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    21
33696
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    22
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    23
HOL-datatype: HOL $(LOG)/HOL-datatype.gz
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    24
33696
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    25
$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML		\
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    26
  HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy	\
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    27
  HOL-datatype/SML.thy HOL-datatype/Verilog.thy
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    28
	@$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    29
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    30
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    31
## HOL-record
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    32
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    33
HOL-record: HOL $(LOG)/HOL-record.gz
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    34
33696
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    35
$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML	\
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    36
   HOL-record/RecordBenchmark.thy
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    37
	@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
2c7c79ca6c23 more accurate dependencies;
wenzelm
parents: 33693
diff changeset
    38
7371
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    39
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    40
## clean
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    41
b176626f0d80 *** empty log message ***
wenzelm
parents:
diff changeset
    42
clean:
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents: 28500
diff changeset
    43
	@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz