diff --git a/tests/playground/parser/Makefile b/tests/playground/parser/Makefile new file mode 100644 index 0000000000..4f983861f7 --- /dev/null +++ b/tests/playground/parser/Makefile @@ -0,0 +1,40 @@ +LEANC=../../../bin/leanc +LEAN=../../../bin/lean +SRCS = $(shell ls *.lean) +OLEANS = $(SRCS:.lean=.olean) +CPPS = $(SRCS:.lean=.cpp) +OBJS = $(SRCS:.lean=.o) +DEPS = $(SRCS:.lean=.depend) +CPPFLAGS = -O3 + +.PHONY: all clean + +all: parser $(OLEANS) + +depends: $(DEPS) + +%.depend: %.lean + @echo $(<:.lean=.olean): `$(LEAN) --deps $< | python relative.py` > $@ + +%.olean: %.lean %.depend + $(LEAN) --make --cpp="$*.cpp.tmp" $< + mv "$*.cpp.tmp" "$*.cpp" + @touch $*.olean + +%.cpp: %.olean + @ + +%.o: %.cpp + $(LEANC) -c $(CPPFLAGS) -o $@ $< + +parser: $(OBJS) + $(LEANC) -o parser $(OBJS) + +clean: + rm -f *.olean + rm -f *.cpp + rm -f *.o + rm -f *.depend + rm -f parser + +include $(DEPS) diff --git a/tests/playground/parser/leanpkg.path b/tests/playground/parser/leanpkg.path new file mode 100644 index 0000000000..a46b9ab3fb --- /dev/null +++ b/tests/playground/parser/leanpkg.path @@ -0,0 +1,2 @@ +builtin_path +path . \ No newline at end of file diff --git a/tests/playground/parser.lean b/tests/playground/parser/parser.lean similarity index 100% rename from tests/playground/parser.lean rename to tests/playground/parser/parser.lean diff --git a/tests/playground/parser/relative.py b/tests/playground/parser/relative.py new file mode 100644 index 0000000000..dda8667a84 --- /dev/null +++ b/tests/playground/parser/relative.py @@ -0,0 +1,9 @@ +# Copyright (c) 2018 Microsoft Corporation. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# Authors: Simon Hudon + +import sys +import os + +for x in sys.stdin: + print(os.path.relpath(x))