Update cc calls in makefiles

Author: oskarabrahamsson

compiler/bootstrap/compilation/arm8/Makefile

@@ -29,7 +29,7 @@ ifeq ($(OS),Darwin)
 endif
 
 CFLAGS+=-O2
-LDFLAGS+=-lm
+LDLIBS+=-lm
 CMLS = $(wildcard *.cml)
 CML_PROGS = $(patsubst %.cml,%.cake$(SUFF),$(CMLS))
 
@@ -39,7 +39,7 @@ all: cake$(SUFF)
 # Linking the CakeML compiler. On aarch
 
 cake$(SUFF): cake.S basis_ffi.c
-	$(CC) $(CFLAGS) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) $(EVALFLAG) -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $< basis_ffi.c $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS)
 
 # Note: While this Makefile is shared the sexpr files used in the example rules
 # below are only included in the verified cake-arm8-64.tar.gz release package
@@ -49,20 +49,20 @@ cake$(SUFF): cake.S basis_ffi.c
 
 cake_verbose$(SUFF): cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --emit_empty_ffi=true --reg_alg=0 < $< > $<.S
-	$(CC) $(CFLAGS) -DDEBUG_FFI -o $@ $<.S basis_ffi.c $(LDFLAGS)
+	$(CC) $(CFLAGS) -DDEBUG_FFI -o $@ $<.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # *UNVERIFIED* compiler supporting 32-bit targets; see cake-arm8-32.tar.gz for a
 # verified compiler
 
 cake_unverified32$(SUFF): cake-sexpr-32 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --reg_alg=0 < $< > $<.S
-	$(CC) $(CFLAGS) -o $@ $<.S basis_ffi.c $(LDFLAGS)
+	$(CC) $(CFLAGS) -o $@ $<.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # Example of cross-compiling the compiler itself
 RISCV_CC ?= riscv64-unknown-linux-gnu-cc
 cake_riscv_host: cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --target=riscv --reg_alg=0 < $< > $<.riscv.S
-	$(RISCV_CC) $(CFLAGS) -o $@ $<.riscv.S basis_ffi.c $(LDFLAGS)
+	$(RISCV_CC) $(CFLAGS) -o $@ $<.riscv.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # Using the CakeML compiler
 
@@ -77,7 +77,7 @@ cake_riscv_host: cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	$(PREF)cake$(SUFF) $(CAKEFLAGS) --target=arm8 <$< >$@
 
 %.cake$(SUFF) : %.cake.S basis_ffi.c
-	$(CC) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS)
+	$(CC) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS) $(LDLIBS)
 
 clean:
 	$(RM) basis_ffi.o cake.o cake$(SUFF) *.cake.o *.cake.S *.cake$(SUFF)

compiler/bootstrap/compilation/x64/Makefile

@@ -27,7 +27,7 @@ ifeq ($(OS),Darwin)
 endif
 
 CFLAGS+=-O2
-LDFLAGS+=-lm
+LDLIBS+=-lm
 CMLS = $(wildcard *.cml)
 CML_PROGS = $(patsubst %.cml,%.cake$(SUFF),$(CMLS))
 
@@ -37,7 +37,7 @@ all: cake$(SUFF)
 # Linking the CakeML compiler
 
 cake$(SUFF): cake.S basis_ffi.c
-	$(CC) $(CFLAGS) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) $(EVALFLAG) -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $< basis_ffi.c $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS)
 
 # Note: While this Makefile is shared the sexpr files used in the example rules
 # below are only included in the verified cake-x64-64.tar.gz release package
@@ -47,20 +47,20 @@ cake$(SUFF): cake.S basis_ffi.c
 
 cake_verbose$(SUFF): cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --emit_empty_ffi=true --reg_alg=0 < $< > $<.S
-	$(CC) $(CFLAGS) -DDEBUG_FFI -o $@ $<.S basis_ffi.c $(LDFLAGS)
+	$(CC) $(CFLAGS) -DDEBUG_FFI -o $@ $<.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # *UNVERIFIED* compiler supporting 32-bit targets; see cake-x64-32.tar.gz for a
 # verified compiler
 
 cake_unverified32$(SUFF): cake-sexpr-32 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --reg_alg=0 < $< > $<.S
-	$(CC) $(CFLAGS) -o $@ $<.S basis_ffi.c $(LDFLAGS)
+	$(CC) $(CFLAGS) -o $@ $<.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # Example of cross-compiling the compiler itself
 RISCV_CC ?= riscv64-unknown-linux-gnu-cc
 cake_riscv_host: cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 $(PREF)cake$(SUFF) --sexp=true --exclude_prelude=true --skip_type_inference=true --target=riscv --reg_alg=0 < $< > $<.riscv.S
-	$(RISCV_CC) $(CFLAGS) -o $@ $<.riscv.S basis_ffi.c $(LDFLAGS)
+	$(RISCV_CC) $(CFLAGS) -o $@ $<.riscv.S basis_ffi.c $(LDFLAGS) $(LDLIBS)
 
 # Using the CakeML compiler
 
@@ -75,7 +75,7 @@ cake_riscv_host: cake-sexpr-64 basis_ffi.c cake$(SUFF)
 	$(PREF)cake$(SUFF) $(CAKEFLAGS) <$< >$@
 
 %.cake$(SUFF) : %.cake.S basis_ffi.c
-	$(CC) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS)
+	$(CC) $< basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS) $(LDLIBS)
 
 clean:
 	$(RM) basis_ffi.o cake.o cake$(SUFF) *.cake.o *.cake.S *.cake$(SUFF)

examples/compilation/x64/Holmakefile

@@ -16,33 +16,37 @@ endif
 ifndef CC
 CC=gcc
 endif
+
+CFLAGS+=-O2
+LDLIBS+=-lm
+
 cat.S: *catCompileScript.sml
 cake_cat: cat.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 grep.S: *grepCompileScript.sml
 cake_grep: grep.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 patch.S: *patchCompileScript.sml
 cake_patch: patch.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 diff.S: *diffCompileScript.sml
 cake_diff: diff.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 hello.S: *helloCompileScript.sml
 cake_hello: hello.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 sort.S: *sortCompileScript.sml
 cake_sort: sort.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 echo.S: *echoCompileScript.sml
 cake_echo: echo.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 helloErr.S: *helloErrCompileScript.sml
 cake_helloErr: helloErr.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 iocat.S: *iocatCompileScript.sml
 cake_iocat: iocat.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 
 exec: cake_cat cake_grep cake_patch cake_diff cake_hello cake_sort cake_echo cake_helloErr cake_iocat
 .PHONY: exec

examples/deflate/translation/compilation/Holmakefile

@@ -1,4 +1,10 @@
-INCLUDES = $(CAKEMLDIR)/examples/deflate  $(CAKEMLDIR)/examples/deflate/translation $(CAKEMLDIR)/compiler $(CAKEMLDIR)/cv_translator
+INCLUDES=$(CAKEMLDIR)/examples/deflate\
+		 $(CAKEMLDIR)/examples/deflate/translation\
+		 $(CAKEMLDIR)/compiler\
+		 $(CAKEMLDIR)/cv_translator
+
+CFLAGS+=-O2
+LDLIBS+=-lm
 
 all: $(DEFAULT_TARGETS) README.md
 
@@ -19,16 +25,16 @@ deflateEncode.S: deflateEncodeCompileScript.sml
 deflateDecode.S: deflateDecodeCompileScript.sml
 
 compression: compression.S
-	gcc -o compression compression.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $< $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 decompression: decompression.S
-	gcc -o decompression decompression.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $< $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 deflateEncode: deflateEncode.S
-	gcc -o deflateEncode deflateEncode.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $< $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 deflateDecode: deflateDecode.S
-	gcc -o deflateDecode deflateDecode.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $< $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 cleanBin:
 	rm -f compression.S decompression.S deflateDecode.S deflateEncode.S compression decompression deflateDecode deflateEncode

examples/opentheory/compilation/Holmakefile

@@ -3,6 +3,9 @@ INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/cv_translator $(CAKEMLDIR)/compiler $(
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all
 
+CFLAGS+=-O2
+LDLIBS+=-lm
+
 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)
@@ -13,6 +16,6 @@ HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
 endif
 
 reader: reader.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
+	$(CC) $(CFLAGS) -o $@ $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(LDLIBS)
 
 EXTRA_CLEANS=reader reader.S

examples/sat_encodings/translation/compilation/Holmakefile

@@ -11,17 +11,20 @@ ifdef POLY
 HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
 endif
 
+CFLAGS+=-O2
+LDLIBS+=-lm
+
 graphColoring_encoder: graphColoringEncoderCompileTheory.uo
-	gcc -o graphColoring_encoder graphColoring_encoder.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 killerSudoku_encoder: killerSudokuEncoderCompileTheory.uo
-	gcc -o killerSudoku_encoder killerSudoku_encoder.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 nQueens_encoder: nQueensEncoderCompileTheory.uo
-	gcc -o nQueens_encoder nQueens_encoder.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 numBoolRange_encoder: numBoolRangeEncoderCompileTheory.uo
-	gcc -o numBoolRange_encoder numBoolRange_encoder.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)
 
 sudoku_encoder: sudokuEncoderCompileTheory.uo
-	gcc -o sudoku_encoder sudoku_encoder.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)

examples/vipr/compilation/Holmakefile

@@ -11,5 +11,8 @@ ifdef POLY
 HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
 endif
 
+CFLAGS+=-O2
+LDLIBS+=-lm
+
 cake_vipr: viprCompileTheory.uo
-	gcc -o cake_vipr cake_vipr.S $(CAKEMLDIR)/basis/basis_ffi.c
+	$(CC) $(CFLAGS) -o $@ $@.S $(CAKEMLDIR)/basis/basis_ffi.c $(LDLIBS)