1#
2# Copyright 2014, NICTA
3#
4# This software may be distributed and modified according to the terms of
5# the BSD 2-Clause license. Note that NO WARRANTY is provided.
6# See "LICENSE_BSD2.txt" for details.
7#
8# @TAG(NICTA_BSD)
9#
10#
11# Common build targets for Isabelle Makefiles.
12#
13# This file should be included after defining a "HEAPS" variable containing the
14# name of all Isabelle heaps that can be built.
15#
16
17# Get path to the base of the repository.
18L4V_REPO_PATH := $(realpath $(dir $(lastword $(MAKEFILE_LIST)))..)
19
20ROOT_ADD ?= ""
21ROOT_PATH := $(L4V_REPO_PATH)$(ROOT_ADD)
22
23# Ensure "ISABELLE_*" environment variables are setup.
24ifndef ISABELLE_HOME
25  export ISABELLE_HOME=${L4V_REPO_PATH}/isabelle
26endif
27ifndef ISABELLE_TOOL
28  export ISABELLE_TOOL=${ISABELLE_HOME}/bin/isabelle
29endif
30ifndef ISABELLE_PROCESS
31  export ISABELLE_PROCESS=${ISABELLE_HOME}/bin/isabelle-process
32endif
33ifndef ISABELLE_OUTPUT
34  export ISABELLE_OUTPUT=$(shell ${ISABELLE_TOOL} getenv -b ISABELLE_OUTPUT)
35endif
36ifndef L4V_ARCH
37  export L4V_ARCH=ARM
38endif
39
40ifdef BUILD_CACHE
41  ISABELLE_BUILD_OPTS=-o "save_skip_cache=true"
42else
43  ISABELLE_BUILD_OPTS=
44endif
45
46# Setup rules for the heaps.
47$(HEAPS): .FORCE
48	$(ISABELLE_TOOL) build -b -v ${ISABELLE_BUILD_OPTS} -d $(ROOT_PATH) $@
49.PHONY: $(HEAPS)
50
51$(GROUPS): .FORCE
52	$(ISABELLE_TOOL) build -b -v ${ISABELLE_BUILD_OPTS} -d $(ROOT_PATH) -g $@
53.PHONY: $(GROUPS)
54
55clean: clean-images
56.PHONY: clean
57
58clean-images:
59	rm -f $(HEAPS:%=$(ISABELLE_OUTPUT)/%)
60	rm -f $(HEAPS:%=$(ISABELLE_OUTPUT)/log/%.gz)
61	rm -f $(HEAPS:%=$(ISABELLE_OUTPUT)/log/%)
62.PHONY: clean-images
63
64realclean: clean
65	rm -rf $(ISABELLE_OUTPUT)
66.PHONY: realclean
67
68#
69# Some targets within this Makefile depend on files, which are managed
70# by independent subprojects (namely, Isabelle and the seL4 kernel).
71# This Makefile is NOT aware of the respective dependencies.  Rather, it
72# forces a recursive call of the corresponding subproject's Makefile
73# whenever a target depends on files managed by a subproject.  For this
74# purpose, we use the special phony target ".FORCE".
75#
76.PHONY: .FORCE
77.FORCE:
78
79# Common targets that should be considered PHONY.
80.PHONY: all default images test
81
82