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

#
# $Id$
#

## targets

default: HOL-datatype
images:
test: HOL-datatype HOL-record
all: images test


## global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log


## HOL-datatype

HOL:
	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL

HOL-datatype: HOL $(LOG)/HOL-datatype.gz

$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/Brackin.thy \
  HOL-datatype/Instructions.thy HOL-datatype/SML.thy \
  HOL-datatype/Verilog.thy
	@$(ISABELLE_TOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype

HOL-record: HOL $(LOG)/HOL-record.gz

$(LOG)/HOL-record.gz: HOL-record/RecordBenchmark.thy 
	@$(ISABELLE_TOOL) usedir -s HOL-record $(OUT)/HOL HOL-record

## clean

clean:
	@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz