From 36e040ecfa1d05caad354a0db0908ffaba15926c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 19 May 2020 12:30:53 +0200
Subject: [PATCH] test: reimplement compiler/foreign on top of leanmake

---
 tests/compiler/foreign/Makefile    | 61 +++++-------------------------
 tests/compiler/foreign/README.md   | 14 ++-----
 tests/compiler/foreign/myfuns.cpp  |  4 +-
 tests/compiler/foreign/relative.py | 14 -------
 4 files changed, 15 insertions(+), 78 deletions(-)
 delete mode 100644 tests/compiler/foreign/relative.py

diff --git a/tests/compiler/foreign/Makefile b/tests/compiler/foreign/Makefile
index 50f748bf57..45da3f421c 100644
--- a/tests/compiler/foreign/Makefile
+++ b/tests/compiler/foreign/Makefile
@@ -1,56 +1,15 @@
-LEAN_BIN=$(LEAN_ROOT)/bin
-LEAN=$(LEAN_BIN)/lean
-LEANC=$(LEAN_BIN)/leanc
-PROJECT_ROOT=.
-SRCS = $(shell cd $(PROJECT_ROOT); find . -name '*.lean')
-OUT ?= out
-DEPS = $(addprefix $(OUT)/,$(SRCS:.lean=.depend))
-OBJS = $(SRCS:.lean=.olean)
-C_LEAN_OBJS = $(addprefix $(OUT)/,$(SRCS:.lean=.o))
-ESC_OUT=$(subst /,\\/,$(OUT))
-CPPFLAGS = -I$(HOME)/lean/lean4/src -O3
+PKG = main
+CPPFLAGS = -O3
+include lean.mk
+
 CPP_SRCS = myfuns.cpp
-CPP_OBJS = $(addprefix $(OUT)/,$(CPP_SRCS:.cpp=.o))
+CPP_OBJS = $(addprefix $(OUT)/testcpp/,$(CPP_SRCS:.cpp=.o))
 
-.PHONY: all clean version dump_out
+all: $(BIN_OUT)/test
 
-all: $(C_LEAN_OBJS) $(CPP_OBJS) $(OUT)/test
-
-depends: $(DEPS)
-
-$(OUT)/%.depend: %.lean
-	@mkdir -p $(OUT)
-	@ deps=`$(LEAN) --deps $< | python relative.py`; echo $(<:.lean=.olean): $$deps > $@
-
-%.olean: %.lean $(addprefix $(OUT)/,%.depend)
-	@echo "[    ] Building $<"
-	@mkdir -p $(OUT)/$(*D)
-	@LEAN_PATH=INI=$(LEAN_ROOT)/src/Init:Proj=$(PROJECT_ROOT) $(LEAN) --make --c="$(OUT)/$*.c.tmp" $<
-	@mv "$(OUT)/$*.c.tmp" "$(OUT)/$*.c"
-	@touch $@
-
-$(OUT)/%.c: %.olean
-	@
-
-$(OUT)/%.o: $(OUT)/%.c
-	@echo "[    ] Building $<"
+$(OUT)/testcpp/%.o: %.cpp
 	@mkdir -p "$(@D)"
-	@ $(LEANC) -c -o $@ $< $(LEANC_OPTS) $(CPPFLAGS)
+	c++ -c -o $@ $< $(CPPFLAGS) `leanc -print-cflags`
 
-$(OUT)/%.o: %.cpp
-	@echo "[    ] Building $<"
-	@mkdir -p "$(@D)"
-	@ $(LEANC) -c -o $@ $< $(LEANC_OPTS) $(CPPFLAGS)
-
-$(OUT)/test: $(C_LEAN_OBJS) $(CPP_OBJS)
-	@ $(LEANC) -o $(OUT)/test $(C_LEAN_OBJS) $(CPP_OBJS)
-
-clean:
-	rm -rf $(OUT) $(OBJS) $(C_LEAN_OBJS) $(CPP_OBJS) $(OUT)/test
-
-version:
-	$(LEAN) -v
-
-.PRECIOUS: $(OUT)/%.depend $(OUT)/%.c
-
-include $(DEPS)
+$(BIN_OUT)/test: $(LIB_OUT)/libmain.a $(CPP_OBJS) | $(BIN_OUT)
+	c++ -o $@ $^ `leanc -print-ldflags`
diff --git a/tests/compiler/foreign/README.md b/tests/compiler/foreign/README.md
index 8690be2dd5..90a1a77156 100644
--- a/tests/compiler/foreign/README.md
+++ b/tests/compiler/foreign/README.md
@@ -6,18 +6,10 @@ The file `main.lean` contains a small Lean program that uses the exported primit
 Build instructions
 =====
 
-The command
-```
-LEAN_ROOT=<your lean4 directory> make
-```
-creates the executable `out/test`.
+Assuming the Lean `bin/` directory (e.g. from `build/release/stage0.5`) is in your `PATH`,
+executing `leanmake` will create the executable `build/bin/test`.
 
-Example:
-```
-LEAN_ROOT=/Users/leonardodemoura/projects/lean4 make
-```
-
-The executable `out/test` should produce the output
+The executable `build/bin/test` should produce the output
 ```
 30
 hello
diff --git a/tests/compiler/foreign/myfuns.cpp b/tests/compiler/foreign/myfuns.cpp
index b3613acf1c..7ddd3a0f2a 100644
--- a/tests/compiler/foreign/myfuns.cpp
+++ b/tests/compiler/foreign/myfuns.cpp
@@ -1,5 +1,5 @@
-#include "runtime/object.h"
-#include "runtime/io.h"
+#include <lean/runtime/object.h>
+#include <lean/runtime/io.h>
 
 struct S {
     unsigned    m_x;
diff --git a/tests/compiler/foreign/relative.py b/tests/compiler/foreign/relative.py
deleted file mode 100644
index c4f8b4b615..0000000000
--- a/tests/compiler/foreign/relative.py
+++ /dev/null
@@ -1,14 +0,0 @@
-# Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-# Released under Apache 2.0 license as described in the file LICENSE.
-# Authors: Simon Hudon, Sebastian Ullrich
-
-import sys
-import os
-import re
-
-for x in sys.stdin:
-  # HACK: rewrite Windows path to mingw path
-  x = re.sub(r"^(\w):", lambda m: "/" + m[1].lower(), x).replace('\\', '/').strip()
-  curr = os.path.realpath(os.curdir)
-  curr = os.path.normpath(curr)
-  print(os.path.relpath(x, curr))