ProgTutorial/Helper/IsaMakefile
author Norbert Schirmer <norbert.schirmer@web.de>
Wed, 22 May 2019 12:38:51 +0200
changeset 574 034150db9d91
parent 321 e450fa467e3f
permissions -rw-r--r--
polish document
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
320
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
## targets
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
default: Command
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
images: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
test: Command
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
all: images test
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
## global settings
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
SRC = $(ISABELLE_HOME)/src
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
OUT = $(ISABELLE_OUTPUT)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
LOG = $(OUT)/log
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf  ## -D generated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
## Command
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
Command: $(LOG)/HOL-Command.gz
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
321
e450fa467e3f polished the commands section
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
    24
$(LOG)/HOL-Command.gz: Command/ROOT.ML Command/*.thy
320
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
	@$(USEDIR) HOL Command
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
## clean
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
clean:
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
	@rm -f $(LOG)/HOL-Command.gz