| author | wenzelm | 
| Mon, 02 May 2011 17:28:09 +0200 | |
| changeset 42620 | 3a9723fca75c | 
| parent 33696 | 2c7c79ca6c23 | 
| child 44640 | 3e666dcdcd32 | 
| permissions | -rw-r--r-- | 
| 7371 | 1 | |
| 2 | ## targets | |
| 3 | ||
| 33696 | 4 | default: all | 
| 7371 | 5 | images: | 
| 33693 
9d76c8080aea
added benchmark for large records
 schirmer <schirmer@in.tum.de> parents: 
28500diff
changeset | 6 | test: HOL-datatype HOL-record | 
| 7371 | 7 | all: images test | 
| 8 | ||
| 9 | ||
| 10 | ## global settings | |
| 11 | ||
| 12 | SRC = $(ISABELLE_HOME)/src | |
| 13 | OUT = $(ISABELLE_OUTPUT) | |
| 14 | LOG = $(OUT)/log | |
| 15 | ||
| 16 | ||
| 17 | ## HOL-datatype | |
| 18 | ||
| 19 | HOL: | |
| 28500 | 20 | @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL | 
| 7371 | 21 | |
| 33696 | 22 | |
| 7371 | 23 | HOL-datatype: HOL $(LOG)/HOL-datatype.gz | 
| 24 | ||
| 33696 | 25 | $(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML \ | 
| 26 | HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy \ | |
| 27 | HOL-datatype/SML.thy HOL-datatype/Verilog.thy | |
| 28 | @$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype | |
| 29 | ||
| 30 | ||
| 31 | ## HOL-record | |
| 7371 | 32 | |
| 33693 
9d76c8080aea
added benchmark for large records
 schirmer <schirmer@in.tum.de> parents: 
28500diff
changeset | 33 | HOL-record: HOL $(LOG)/HOL-record.gz | 
| 
9d76c8080aea
added benchmark for large records
 schirmer <schirmer@in.tum.de> parents: 
28500diff
changeset | 34 | |
| 33696 | 35 | $(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML \ | 
| 36 | HOL-record/RecordBenchmark.thy | |
| 37 | @$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record | |
| 38 | ||
| 7371 | 39 | |
| 40 | ## clean | |
| 41 | ||
| 42 | clean: | |
| 33693 
9d76c8080aea
added benchmark for large records
 schirmer <schirmer@in.tum.de> parents: 
28500diff
changeset | 43 | @rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz |