Improve root directory organisation

Closes #164

Author: xrchz

Holmakefile

@@ -1,22 +1,13 @@
-INCLUDES = developers $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub lem_lib_stub $(HOLDIR)/examples/machine-code/hoare-triple
+INCLUDES = developers compiler/bootstrap/evaluation/x64
 OPTIONS = QUIT_ON_FAILURE
 
-README_SOURCES = miscScript.sml COPYING developers build-instructions.sh lib.lem libScript.sml
+README_SOURCES = COPYING developers build-instructions.sh
 
-THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
-TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
-TARGETS = README.md $(patsubst %.sml,%.uo,$(TARGETS0))
-all: $(TARGETS)
+all: README.md cake
 .PHONY: all
 
-LEMSRC = lib
-LEMS = $(patsubst %,%.lem,$(LEMSRC))
-GENS = $(patsubst %,%Script.sml,$(LEMSRC))
-
-README.md: $(README_SOURCES) readmePrefix
+README.md: $(README_SOURCES) readmePrefix developers/readme_gen
 	developers/readme_gen $(README_SOURCES)
 
-$(GENS): $(LEMS)
-	if type lem;\
-	then lem $(LEM_OPT) -suppress_renaming -auxiliary_level none -hol $(LEMS);\
-	else touch $(GENS); fi
+cake: compiler/bootstrap/evaluation/x64/cake
+	$(CP) $< $@

README.md

@@ -1,4 +1,4 @@
-INCLUDES = .. pure ../translator ../characteristic ../semantics
+INCLUDES = ../misc pure ../translator ../characteristic ../semantics
 OPTIONS = QUIT_ON_FAILURE
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))

basis/Holmakefile

@@ -1,2 +1,2 @@
-INCLUDES = ../.. $(HOLDIR)/examples/fun-op-sem/lprefix_lub $(HOLDIR)/examples/formal-languages/regular
+INCLUDES = ../../misc $(HOLDIR)/examples/formal-languages/regular
 OPTIONS = QUIT_ON_FAILURE

basis/pure/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../.. $(HOLDIR)/examples/set-theory/hol_sets
+INCLUDES = ../../misc $(HOLDIR)/examples/set-theory/hol_sets
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -10,7 +10,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = $(HOLDIR)/examples/set-theory/hol_sets/cardinalTheory ../../miscTheory
+BARE_THYS = $(HOLDIR)/examples/set-theory/hol_sets/cardinalTheory ../../misc/miscTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

candle/set-theory/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../../semantics ../../../semantics/alt_semantics ../../../translator ../monadic ../../../explorer/pp/astPP ../../../characteristic ../../../basis ../../../translator/monadic
+INCLUDES = ../../../misc ../../../semantics ../../../semantics/alt_semantics ../../../translator ../monadic ../../../explorer/pp/astPP ../../../characteristic ../../../basis ../../../translator/monadic
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../preamble ../monadic/holKernelTheory
+BARE_THYS = ../../../misc/preamble ../monadic/holKernelTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

candle/standard/ml_kernel/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../syntax-lib ../syntax ../../../translator/monadic/
+INCLUDES = ../../../misc ../../syntax-lib ../syntax ../../../translator/monadic/
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../preamble ../../syntax-lib/holSyntaxLibTheory ../syntax/holAxiomsSyntaxTheory
+BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory ../syntax/holAxiomsSyntaxTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

candle/standard/monadic/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../monadic
+INCLUDES = ../../../misc ../monadic

candle/standard/opentheory/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../../basis/pure ../../syntax-lib ../../set-theory ../syntax
+INCLUDES = ../../../misc ../../../basis/pure ../../syntax-lib ../../set-theory ../syntax
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../preamble ../../syntax-lib/holSyntaxLibTheory ../../set-theory/setSpecTheory ../syntax/holAxiomsSyntaxTheory
+BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory ../../set-theory/setSpecTheory ../syntax/holAxiomsSyntaxTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

candle/standard/semantics/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../syntax-lib
+INCLUDES = ../../../misc ../../syntax-lib
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -10,7 +10,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../preamble ../../syntax-lib/holSyntaxLibTheory
+BARE_THYS = ../../../misc/preamble ../../syntax-lib/holSyntaxLibTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

candle/standard/syntax/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../.. $(HOLDIR)/examples/fun-op-sem/lprefix_lub ../../basis/pure
+INCLUDES = ../../misc ../../basis/pure

candle/syntax-lib/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = .. ../semantics ../semantics/alt_semantics/proofs ../lem_lib_stub ../explorer/pp/astPP ../translator $(HOLDIR)/examples/machine-code/hoare-triple ../compiler/parsing
+INCLUDES = ../misc ../semantics ../semantics/alt_semantics/proofs ../explorer/pp/astPP ../translator $(HOLDIR)/examples/machine-code/hoare-triple ../compiler/parsing
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY

characteristic/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = .. ../../.. ../../../basis ../../../compiler
+INCLUDES = .. ../../../misc ../../../basis ../../../compiler
 CLINE_OPTIONS = -j1 --qof
 TARGETS = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 all: $(TARGETS)

characteristic/examples/compilation/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../../../semantics/proofs ../../../.. .. ../.. ../../../../compiler/backend/proofs ../../../../compiler/encoders/x64/proofs ../../../../compiler/backend/x64/proofs
+INCLUDES = ../../../../semantics/proofs ../../../../misc .. ../.. ../../../../compiler/backend/proofs ../../../../compiler/encoders/x64/proofs ../../../../compiler/backend/x64/proofs
 CLINE_OPTIONS = -j1 --qof
 ifdef POLY
 HOLHEAP=../heap

characteristic/examples/compilation/proofs/Holmakefile

@@ -1,5 +1,5 @@
 OPTIONS = QUIT_ON_FAILURE
-INCLUDES = .. ../semantics parsing inference backend\
+INCLUDES = ../misc ../semantics parsing inference backend\
 					 backend/reg_alloc encoders/asm\
 					 ../basis\
 					 backend/arm6 backend/arm8\

compiler/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../.. ../../semantics ../../basis/pure ../encoders ../encoders/asm reg_alloc $(HOLDIR)/examples/machine-code/multiword
+INCLUDES = ../../misc ../../semantics ../../basis/pure ../encoders ../encoders/asm reg_alloc $(HOLDIR)/examples/machine-code/multiword
 
 OPTIONS = QUIT_ON_FAILURE
 

compiler/backend/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../../../basis/pure .. ../../encoders/arm6
+INCLUDES = ../../../misc ../../../basis/pure .. ../../encoders/arm6

compiler/backend/arm6/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../../.. .. ../../../encoders/arm6/proofs ../../semantics ../../proofs
+INCLUDES = ../../../../misc .. ../../../encoders/arm6/proofs ../../semantics ../../proofs

compiler/backend/arm6/proofs/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../../../basis/pure .. ../../encoders/arm8
+INCLUDES = ../../../misc ../../../basis/pure .. ../../encoders/arm8

compiler/backend/arm8/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../../.. .. ../../../encoders/arm8/proofs ../../semantics ../../proofs
+INCLUDES = ../../../../misc .. ../../../encoders/arm8/proofs ../../semantics ../../proofs

compiler/backend/arm8/proofs/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ..
+INCLUDES = ../../../misc ..
 
 OPTIONS = QUIT_ON_FAILURE
 
@@ -13,7 +13,7 @@ HOLHEAP = heap
 EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
 all: $(HOLHEAP)
 
-BARE_THYS = ../../../preamble
+BARE_THYS = ../../../misc/preamble
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
 $(HOLHEAP): $(DEPS)

compiler/backend/gc/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../../../basis/pure .. ../../encoders/mips
+INCLUDES = ../../../misc ../../../basis/pure .. ../../encoders/mips

compiler/backend/mips/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../../.. .. ../../../encoders/mips/proofs ../../semantics ../../proofs
+INCLUDES = ../../../../misc .. ../../../encoders/mips/proofs ../../semantics ../../proofs

compiler/backend/mips/proofs/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = .. ../semantics ../../.. ../../../semantics ../../../semantics/proofs ../../encoders ../reg_alloc/proofs ../gc $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/machine-code/multiword
+INCLUDES = .. ../semantics ../../../misc ../../../semantics ../../../semantics/proofs ../../encoders ../reg_alloc/proofs ../gc $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/machine-code/multiword
 
 OPTIONS = QUIT_ON_FAILURE
 

compiler/backend/proofs/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../../unverified/reg_alloc $(HOLDIR)/examples/fun-op-sem/lprefix_lub
+INCLUDES = ../../../misc ../../../unverified/reg_alloc
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../preamble
+BARE_THYS = ../../../misc/preamble
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
 $(HOLHEAP): $(DEPS)

compiler/backend/reg_alloc/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ..  ../../../..
+INCLUDES = ..  ../../../../misc
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS = ../../../../preamble ../reg_allocTheory
+BARE_THYS = ../../../../misc/preamble ../reg_allocTheory
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
 $(HOLHEAP): $(DEPS)

compiler/backend/reg_alloc/proofs/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../../../basis/pure .. ../../encoders/riscv
+INCLUDES = ../../../misc ../../../basis/pure .. ../../encoders/riscv

compiler/backend/riscv/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../../.. .. ../../../encoders/riscv/proofs ../../semantics ../../proofs
+INCLUDES = ../../../../misc .. ../../../encoders/riscv/proofs ../../semantics ../../proofs

compiler/backend/riscv/proofs/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = .. ../../.. ../../../semantics ../../../semantics/proofs ../../encoders/asm
+INCLUDES = .. ../../../misc ../../../semantics ../../../semantics/proofs ../../encoders/asm
 
 OPTIONS = QUIT_ON_FAILURE
 

compiler/backend/semantics/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../.. ../../../basis/pure .. ../../encoders/x64
+INCLUDES = ../../../misc ../../../basis/pure .. ../../encoders/x64

compiler/backend/x64/Holmakefile

@@ -1 +1 @@
-INCLUDES = ../../../.. .. ../../../encoders/x64/proofs ../../semantics ../../proofs
+INCLUDES = ../../../../misc .. ../../../encoders/x64/proofs ../../semantics ../../proofs

compiler/backend/x64/proofs/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../../translator ../../../characteristic ../../inference ../../inference/proofs ../../parsing ../../backend ../.. \
+INCLUDES = ../../../misc ../../../translator ../../../characteristic ../../inference ../../inference/proofs ../../parsing ../../backend ../.. \
 					 ../../backend/reg_alloc ../../backend/reg_alloc/proofs ../../../basis ../../../explorer/pp/astPP
 OPTIONS = QUIT_ON_FAILURE
 

compiler/bootstrap/translation/Holmakefile

@@ -1,2 +1,2 @@
 OPTIONS = QUIT_ON_FAILURE
-INCLUDES = ../../.. $(HOLDIR)/examples/l3-machine-code/common $(HOLDIR)/examples/fun-op-sem/lprefix_lub ../../../semantics
+INCLUDES = ../../../misc $(HOLDIR)/examples/l3-machine-code/common ../../../semantics

compiler/encoders/asm/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES=../.. ../../semantics ../../semantics/proofs $(HOLDIR)/examples/unification/triangular/first-order ../../basis/pure
+INCLUDES = ../../misc ../../semantics ../../semantics/proofs $(HOLDIR)/examples/unification/triangular/first-order ../../basis/pure
 OPTIONS = QUIT_ON_FAILURE
 
 SEMANTICSI = semanticPrimitives

compiler/inference/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES=.. ../../.. ../../../semantics ../../../semantics/proofs
+INCLUDES = .. ../../../misc ../../../semantics ../../../semantics/proofs
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY

compiler/inference/proofs/Holmakefile

@@ -1,5 +1,5 @@
 SEMANTICS = ../../semantics
-INCLUDES = $(HOLDIR)/examples/formal-languages/context-free ../.. $(SEMANTICS)
+INCLUDES = $(HOLDIR)/examples/formal-languages/context-free ../../misc $(SEMANTICS)
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY

compiler/parsing/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../../.. ../../../semantics
+INCLUDES = ../../../misc ../../../semantics
 
 OPTIONS = QUIT_ON_FAILURE
 

explorer/pp/astPP/Holmakefile

@@ -0,0 +1,6 @@
+INCLUDES = ../developers lem_lib_stub $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/fun-op-sem/lprefix_lub
+
+README_SOURCES = preamble.sml miscScript.sml basicComputeLib.sml
+
+README.md: $(README_SOURCES) readmePrefix ../developers/readme_gen
+	../developers/readme_gen $(README_SOURCES)

misc/Holmakefile

@@ -0,0 +1,15 @@
+INCLUDES = $(HOLDIR)/examples/formal-languages/context-free
+
+LEMSRC = lib
+LEMS = $(patsubst %,%.lem,$(LEMSRC))
+GENS = $(patsubst %,%Script.sml,$(LEMSRC))
+THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
+TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
+TARGETS = $(GENS) $(TARGETS0)
+all: $(TARGETS)
+.PHONY: all
+
+$(GENS): $(LEMS)
+	if type lem;\
+	then lem $(LEM_OPT) -suppress_renaming -auxiliary_level none -hol $(LEMS);\
+	else touch $(GENS); fi

misc/README.md

@@ -0,0 +1,2 @@
+Auxiliary files providing glue between a standard HOL installation
+and what we want to use for CakeML development.

basicComputeLib.sig misc/basicComputeLib.sig

@@ -1,5 +1,5 @@
 OPTIONS = QUIT_ON_FAILURE
-INCLUDES = .. $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub ../lem_lib_stub ffi
+INCLUDES = ../misc $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub ffi
 
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
@@ -14,24 +14,26 @@ SRC = semanticPrimitives evaluate typeSystem primTypes
 LEMS = $(patsubst %,%.lem,$(SRC))
 GENS = $(patsubst %,%Script.sml,$(SRC))
 
-LEM_CMD = lem $(LEM_OPT) -suppress_renaming -auxiliary_level none -i ../lib.lem -i ffi/ffi.lem -hol
+LEMLIB = ../misc/lem_lib_stub/lib.lem
 
-$(GENS): $(LEMS) ../lib.lem ffi/ffi.lem
+LEM_CMD = lem $(LEM_OPT) -suppress_renaming -auxiliary_level none -i $(LEMLIB) -i ffi/ffi.lem -hol
+
+$(GENS): $(LEMS) $(LEMLIB) ffi/ffi.lem
 	if type lem;\
 	then $(LEM_CMD) $(LEMS);\
 	else touch $(GENS); fi
 
-astScript.sml: ast.lem namespace.lem ../lib.lem ffi/ffi.lem addancs
+astScript.sml: ast.lem namespace.lem $(LEMLIB) ffi/ffi.lem addancs
 	if type lem; then \
           $(LEM_CMD) $< ;  ./addancs $@ integer words string namespace location; \
         else touch astScript.sml ; fi
 
-tokensScript.sml: tokens.lem ../lib.lem ffi/ffi.lem addancs
+tokensScript.sml: tokens.lem $(LEMLIB) ffi/ffi.lem addancs
 	if type lem; then \
           $(LEM_CMD) $< ;  ./addancs $@ integer string ; \
         else touch $@ ; fi
 
-namespaceScript.sml: namespace.lem ../lib.lem ffi/ffi.lem addancs
+namespaceScript.sml: namespace.lem $(LEMLIB) ffi/ffi.lem addancs
 	if type lem; then \
           $(LEM_CMD) $< ;  ./addancs $@ integer words string alist; \
         else touch namespaceScript.sml ; fi
@@ -43,7 +45,7 @@ EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o addancs
 GRAMMAR_DEPS0 = peg pegexec
 GRAMMAR_DEPS = $(patsubst %,$(HOLDIR)/examples/formal-languages/context-free/%Theory,$(GRAMMAR_DEPS0))
 
-BARE_THYS = ../preamble $(GRAMMAR_DEPS) ../basicComputeLib ffi/ffiTheory $(HOLDIR)/examples/fun-op-sem/lprefix_lub/lprefix_lubTheory
+BARE_THYS = ../misc/preamble $(GRAMMAR_DEPS) ../misc/basicComputeLib ffi/ffiTheory
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
 all: $(HOLHEAP)