Commit 780f8cd7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix regression test

parent d620d76e
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra
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)
all: $(TARGETS)
.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