max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: reimplement compiler/foreign on top of leanmake

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-19 12:30:53 +02:00 • committed by Leonardo de Moura
parent 573a128096
commit 36e040ecfa
4 changed files with 15 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
tests/compiler/foreign/Makefile
View file

@ -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`

14
tests/compiler/foreign/README.md
View file

@ -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

4
tests/compiler/foreign/myfuns.cpp
View file

@ -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;

14
tests/compiler/foreign/relative.py
View file

@ -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))