Commit 9046ff96 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make binary compilation work with new preambleFloVer to get CML dependencies right

parent 4ee074cf
INCLUDES = .. $(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/backend $(CAKEMLDIR)/misc
INCLUDES = .. ./cakeml/compiler ./cakeml/compiler/backend ./cakeml/misc
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP) cake_checker
#ifdef POLY
#HOLHEAP = heap
#EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
#all: $(HOLHEAP) cake_checker
ifndef CC
CC=gcc
endif
cake_checker: checker.S ../cakeml/basis/basis_ffi.o
$(CC) $< ../cakeml/basis/basis_ffi.o $(GCCFLAGS) -o $@
checker.S: checkerBinaryTheory.uo
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = ../transTheory \
../cakeml/compiler/compilationLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
#ifndef CC
#CC=gcc
#endif
#cake_checker: checker.S ../cakeml/basis/basis_ffi.o
# $(CC) $< ../cakeml/basis/basis_ffi.o $(GCCFLAGS) -o $@
#
#checker.S: checkerBinaryTheory.uo
#
#THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
#TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
#all: $(TARGETS) $(HOLHEAP)
#.PHONY: all
#
#BARE_THYS = ../transTheory \
# ../cakeml/compiler/compilationLib
#
#DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
#
#$(HOLHEAP): $(DEPS)
# $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
#endif
open preamble compilationLib transTheory
open preambleFloVer compilationLib transTheory
val _ = new_theory "checkerBinary"
......
......@@ -5,7 +5,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
ErrorBoundsTheory IntervalArithTheory FloverTactics IntervalValidationTheory
EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory
CertificateCheckerTheory floverParserTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "trans";
......
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