Commit 2e3aaa7d authored by Heiko Becker's avatar Heiko Becker

Add Holmakefile to output directory for HOL4

parent 1aba0115
......@@ -28,6 +28,7 @@ hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/heap
hol4/output/heap
daisy
rawdata/*
.ensime*
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \
combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \
listTheory llistTheory markerLib realTheory realLib RealArith\
optionTheory pairLib pairTheory pred_setTheory \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment