Permalink
Browse files

Clean Holmakefiles in candle and tutorial

  • Loading branch information...
xrchz committed Dec 14, 2018
1 parent f7e0f48 commit b8a75a816615f55dee772a73c70295e55c4b7c1e
@@ -1,8 +1,9 @@
DIRS = $(wildcard */)
INCLUDES =

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,28 +1,9 @@
INCLUDES = ../../misc $(HOLDIR)/src/pred_set/src/more_theories
OPTIONS = QUIT_ON_FAILURE
INCLUDES = $(HOLDIR)/src/pred_set/src/more_theories $(CAKEMLDIR)/misc

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

all: $(TARGETS) $(HOLHEAP)
.PHONY: all

BARE_THYS = $(HOLDIR)/src/pred_set/src/more_theories/cardinalTheory ../../misc/miscTheory

DEPS = $(patsubst %,%.uo,$(BARE_THYS))

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,8 +1,9 @@
INCLUDES =

all: $(DEFAULT_TARGETS) README.md

.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,8 +1,9 @@
DIRS = $(wildcard */)
INCLUDES =

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,29 +1,12 @@
INCLUDES = ../../../misc ../../../semantics ../../../translator ../monadic ../../../characteristic ../../../basis ../../../basis/pure ../../../translator/monadic
OPTIONS = QUIT_ON_FAILURE
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics\
$(CAKEMLDIR)/translator $(CAKEMLDIR)/translator/monadic\
$(CAKEMLDIR)/basis $(CAKEMLDIR)/basis/pure\
$(CAKEMLDIR)/characteristic ../monadic

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = ../monadic/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

all: $(TARGETS) $(HOLHEAP)
.PHONY: all

BARE_THYS = ../../../misc/preamble ../monadic/holKernelTheory

DEPS = $(patsubst %,%.uo,$(BARE_THYS))

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS)
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,29 +1,10 @@
INCLUDES = ../../../misc ../../syntax-lib ../syntax ../../../translator/monadic/
OPTIONS = QUIT_ON_FAILURE
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/translator/monadic\
../../syntax-lib ../syntax

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = ../syntax/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

all: $(TARGETS) $(HOLHEAP)
.PHONY: all

BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory ../syntax/holAxiomsSyntaxTheory

DEPS = $(patsubst %,%.uo,$(BARE_THYS))

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS)
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,38 +1,12 @@
INCLUDES = ../../../misc ../monadic \
../ml_kernel \
../../../basis \
../../../translator/monadic \
../../../characteristic \
../../../semantics \
../semantics
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics\
$(CAKEMLDIR)/basis $(CAKEMLDIR)/translator/monadic\
$(CAKEMLDIR)/characteristic\
../monadic ../semantics ../ml_kernel

all: $(DEFAULT_TARGETS) README.md

OPTIONS = QUIT_ON_FAILURE
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY

HOLHEAP = heap
PARENT_HOLHEAP = ../ml_kernel/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

.PHONY: all
all: $(TARGETS) $(HOLHEAP)

BARE_THYS = ../../../misc/preamble ../monadic/holKernelTheory \
../../../basis/basisProgTheory

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) \
-o $(HOLHEAP) $(BARE_THYS)

endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,18 +1,14 @@
INCLUDES = .. ../../../../compiler ../../../../misc
CLINE_OPTIONS = --qof
TARGETS = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/compiler ..

all: $(DEFAULT_TARGETS) README.md

all: $(TARGETS)
.PHONY: all

reader: reader.S ../../../../basis/basis_ffi.o
$(CC) $< ../../../../basis/basis_ffi.o $(GCCFLAGS) -o $@

EXTRA_CLEANS=reader reader.S

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)

reader: reader.S $(CAKEMLDIR)/basis/basis_ffi.o
$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@

EXTRA_CLEANS=reader reader.S
@@ -1,17 +1,13 @@
INCLUDES = .. ../.. \
../../../../../misc \
../../../../../semantics/proofs \
../../../../../compiler/backend/proofs \
../../../../../compiler/encoders/x64/proofs \
../../../../../compiler/backend/x64/proofs
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics/proofs\
$(CAKEMLDIR)/compiler/backend/proofs\
$(CAKEMLDIR)/compiler/encoders/x64/proofs\
$(CAKEMLDIR)/compiler/backend/x64/proofs\
.. ../..

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP=../../heap
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,8 +1,9 @@
INCLUDES = ..

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,18 +1,14 @@
INCLUDES = .. ../../../../../compiler ../../../../../misc
CLINE_OPTIONS = --qof
TARGETS = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/compiler ..

all: $(DEFAULT_TARGETS) README.md

all: $(TARGETS)
.PHONY: all

readerIO: readerIO.S ../../../../../basis/basis_ffi.c
$(CC) -DDEBUG_FFI $< ../../../../../basis/basis_ffi.c $(GCCFLAGS) -o $@

EXTRA_CLEANS=readerIO readerIO.S

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)

readerIO: readerIO.S $(CAKEMLDIR)/basis/basis_ffi.c
$(CC) -DDEBUG_FFI $< $(protect $(CAKEMLDIR)/basis/basis_ffi.c) $(GCCFLAGS) -o $@

EXTRA_CLEANS=readerIO readerIO.S
@@ -1,29 +1,10 @@
INCLUDES = ../../../misc ../../../basis/pure ../../syntax-lib ../../set-theory ../syntax
OPTIONS = QUIT_ON_FAILURE
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis/pure\
../../syntax-lib ../../set-theory ../syntax

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = ../../set-theory/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

all: $(TARGETS) $(HOLHEAP)
.PHONY: all

BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory ../../set-theory/setSpecTheory ../syntax/holAxiomsSyntaxTheory

DEPS = $(patsubst %,%.uo,$(BARE_THYS))

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS)
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,28 +1,9 @@
INCLUDES = ../../../misc ../../syntax-lib
OPTIONS = QUIT_ON_FAILURE
INCLUDES = $(CAKEMLDIR)/misc ../../syntax-lib

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o

THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))

all: $(TARGETS) $(HOLHEAP)
.PHONY: all

BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory

DEPS = $(patsubst %,%.uo,$(BARE_THYS))

$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,8 +1,9 @@
INCLUDES = ../../misc ../../basis/pure
INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis/pure

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
@@ -1,10 +1,14 @@
INCLUDES = $(HOLDIR)/examples/balanced_bst ../misc ../translator ../basis/pure ../basis ../characteristic ../compiler\
../semantics ../semantics/proofs ../compiler/backend/proofs ../compiler/backend/x64/proofs
CLINE_OPTIONS = --qof
INCLUDES = $(HOLDIR)/examples/balanced_bst\
$(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics $(CAKEMLDIR)/semantics/proofs\
$(CAKEMLDIR)/basis/pure $(CAKEMLDIR)/basis\
$(CAKEMLDIR)/translator $(CAKEMLDIR)/characteristic\
$(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/backend/proofs\
$(CAKEMLDIR)/compiler/backend/x64/proofs

all: $(DEFAULT_TARGETS) README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
DIRS = $(wildcard */)
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
Oops, something went wrong.

0 comments on commit b8a75a8

Please sign in to comment.