Merge pull request #910 from CakeML/minor-tweaks

Minor tweaks
CakeML · Sep 25, 2022 · 8787dfe · 8787dfe
2 parents f28083a + a69ce9e
commit 8787dfe
Show file tree

Hide file tree

Showing 9 changed files with 21 additions and 13 deletions.
diff --git a/basis/basis_ffi.c b/basis/basis_ffi.c
@@ -8,7 +8,7 @@
 #include <unistd.h>
 #include <fcntl.h>
 #include <assert.h>
-#ifdef __EVAL__
+#ifdef EVAL
 #include <sys/time.h>
 #include <sys/stat.h>
 #include <sys/mman.h>
@@ -36,7 +36,7 @@ extern char cake_text_begin;
 extern char cake_codebuffer_begin;
 extern char cake_codebuffer_end;
 
-#ifdef __EVAL__
+#ifdef EVAL
 
 /* Signal handler for SIGINT */
 
@@ -140,7 +140,7 @@ void ffiopen_in (unsigned char *c, long clen, unsigned char *a, long alen) {
 
 void ffiopen_out (unsigned char *c, long clen, unsigned char *a, long alen) {
   assert(9 <= alen);
-  #ifdef __EVAL__
+  #ifdef EVAL
   int fd = open((const char *) c, O_RDWR|O_CREAT|O_TRUNC, S_IRUSR|S_IWUSR|S_IRGRP|S_IROTH);
   #else
   int fd = open((const char *) c, O_RDWR|O_CREAT|O_TRUNC);
@@ -379,7 +379,7 @@ int main (int local_argc, char **local_argv) {
   cml_stack = cml_heap + cml_heap_sz;
   cml_stackend = cml_stack + cml_stack_sz;
 
-  #ifdef __EVAL__
+  #ifdef EVAL
 
   /** Set up the "eval" code buffer to be read-write-execute. **/
   if(mprotect(&cake_text_begin, &cake_codebuffer_end - &cake_text_begin,

diff --git a/compiler/backend/exportScript.sml b/compiler/backend/exportScript.sml
@@ -69,7 +69,7 @@ Definition data_buffer_def:
      MAP (\n. strlit (n ++ "\n"))
        ["     .globl cdecl(cake_bitmaps_buffer_begin)";
         "cdecl(cake_bitmaps_buffer_begin):";
-        "#if defined(__EVAL__)";
+        "#if defined(EVAL)";
         "     .space DATA_BUFFER_SIZE";
         "#endif";
         "     .globl cdecl(cake_bitmaps_buffer_end)";
@@ -81,7 +81,7 @@ Definition code_buffer_def:
      MAP (\n. strlit (n ++ "\n"))
        ["     .globl cdecl(cake_codebuffer_begin)";
         "cdecl(cake_codebuffer_begin):";
-        "#if defined(__EVAL__)";
+        "#if defined(EVAL)";
         "     .space CODE_BUFFER_SIZE";
         "#endif";
         "     .p2align 12";

diff --git a/compiler/bootstrap/compilation/x64/32/Holmakefile b/compiler/bootstrap/compilation/x64/32/Holmakefile
@@ -14,7 +14,7 @@ README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmeP
 
 cake.S: *$(ARCH)BootstrapScript.sml
 
-cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile how-to.md
-	tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile how-to.md
+cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile hello.cml how-to.md
+	tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile hello.cml how-to.md
 
 EXTRA_CLEANS = cake.S cake-$(ARCH)-$(WORD_SIZE).tar.gz
diff --git a/compiler/bootstrap/compilation/x64/32/hello.cml b/compiler/bootstrap/compilation/x64/32/hello.cml
@@ -0,0 +1 @@
+../hello.cml
diff --git a/compiler/bootstrap/compilation/x64/64/Holmakefile b/compiler/bootstrap/compilation/x64/64/Holmakefile
@@ -18,8 +18,8 @@ config_enc_str.txt: *$(ARCH)_config_encScript.sml
 cake-sexpr-32: *sexprBootstrap32Script.sml
 cake-sexpr-64: *sexprBootstrap64Script.sml
 
-cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile how-to.md cake-sexpr-32 cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
-	tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile how-to.md cake-sexpr-32 cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
+cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile hello.cml how-to.md cake-sexpr-32 cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
+	tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile hello.cml how-to.md cake-sexpr-32 cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
 	make test-hello.cake   # the following lines are a basic test
 	./test-hello.cake >output
 	echo 'Hello!'>expected_output

diff --git a/compiler/bootstrap/compilation/x64/64/hello.cml b/compiler/bootstrap/compilation/x64/64/hello.cml
@@ -0,0 +1 @@
+../hello.cml
diff --git a/compiler/bootstrap/compilation/x64/Makefile b/compiler/bootstrap/compilation/x64/Makefile
@@ -17,7 +17,7 @@ ifeq ($(OS),Windows_NT)
 else
 	PREF = ./
 	SUFF =
-	EVALFLAG = -D__EVAL__
+	EVALFLAG = -DEVAL
 endif
 
 ifeq ($(OS),Darwin)

diff --git a/compiler/bootstrap/compilation/x64/hello.cml b/compiler/bootstrap/compilation/x64/hello.cml
@@ -0,0 +1,4 @@
+(*
+   A simple hello world program in CakeML
+*)
+print "Hello, World!\n";
diff --git a/developers/build-sequence b/developers/build-sequence
@@ -4,6 +4,10 @@
 developers
 developers/bin
 
+# build many things in parallel at the start
+compiler/proofs
+compiler/bootstrap/translation
+
 # semantics and metatheory
 semantics/ffi
 semantics
@@ -66,7 +70,6 @@ compiler/backend/arm8_asl
 compiler/backend/mips/proofs
 compiler/backend/riscv/proofs
 compiler/backend/ag32/proofs
-compiler/proofs
 
 # candle
 candle/set-theory
@@ -131,7 +134,6 @@ icing/examples
 
 # compiler translation
 compiler/repl
-compiler/bootstrap/translation
 
 # compiler sexpr bootstrap
 unverified/sexpr-bootstrap/x64/64:cake-unverified-x64-64.tar.gz