Botworld.HOL/Holmakefile at master · machine-intelligence/Botworld.HOL · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
ifndef CAKEMLDIR
CAKEMLDIR = $(HOME)/cakeml
endif

ifndef HOLREFLDIR
HOLREFLDIR = $(HOME)/hol-reflection
endif

CLINE_OPTIONS = --qof

INCLUDES = $(CAKEMLDIR)\
           $(CAKEMLDIR)/semantics\
					 $(CAKEMLDIR)/semantics/proofs\
					 $(CAKEMLDIR)/compiler/parsing\
					 $(CAKEMLDIR)/translator\
					 $(HOLDIR)/examples/formal-languages/context-free\
					 $(CAKEMLDIR)/candle/standard/syntax\
					 $(CAKEMLDIR)/candle/standard/semantics\
					 $(CAKEMLDIR)/candle/standard/monadic\
					 $(HOLREFLDIR) $(HOLREFLDIR)/lca
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS)
.PHONY: all

ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
BARE_THYS = $(CAKEMLDIR)/preamble\
						$(CAKEMLDIR)/semantics/terminationTheory\
						$(CAKEMLDIR)/semantics/proofs/evaluatePropsTheory\
						$(CAKEMLDIR)/compiler/parsing/fromSexpTheory\
						$(CAKEMLDIR)/translator/ml_translatorLib\
						$(CAKEMLDIR)/candle/standard/monadic/holKernelTheory\
						$(HOLREFLDIR)/lca/lcaTheory
DEPS = $(patsubst %,%.uo,$(BARE_THYS))
$(HOLHEAP): $(DEPS)
	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif