diff --git a/library/Makefile.common b/library/Makefile.common new file mode 100644 index 000000000..23d62e715 --- /dev/null +++ b/library/Makefile.common @@ -0,0 +1,25 @@ +TOP := $(dir $(lastword $(MAKEFILE_LIST))) +EXTRACT_DEPS = $(TOP)/extract_deps +LEAN_FILES = $(wildcard *.lean) +OLEAN_FILES = $(LEAN_FILES:.lean=.olean) +DEPS = make.deps + +all: $(OLEAN_FILES) $(DEPS) + +%.olean: %.lean + $(LEAN) $< -o $@ + +%.olean: %.lua + $(LEAN) $< -o $@ + +.PHONY: all clean + +clean: + -rm -f *.olean $(DEPS) + +$(DEPS): $(LEAN_FILES) + LEAN=$(LEAN) $(EXTRACT_DEPS) $(LEAN_FILES) > make.deps + +ifneq ($(MAKECMDGOALS),clean) +-include $(DEPS) +endif diff --git a/library/extract_deps b/library/extract_deps new file mode 100755 index 000000000..dc642aad3 --- /dev/null +++ b/library/extract_deps @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +for LEANFILE in $@; do + OLEANFILE=${LEANFILE//.lean/.olean} + DEPS=`$LEAN --deps $LEANFILE | cut -d ' ' -f 2- | tr "\n" " "` + echo -n "$OLEANFILE:" + for DEP in $DEPS; do + echo -n " ${DEP}" + done + echo "" +done diff --git a/library/standard/Makefile b/library/standard/Makefile new file mode 100644 index 000000000..0a42375f1 --- /dev/null +++ b/library/standard/Makefile @@ -0,0 +1 @@ +include ../Makefile.common diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d6bc1c602..66757ba28 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -270,3 +270,10 @@ file(GLOB_RECURSE LEAN_SOURCES ${LEAN_SOURCE_DIR}/[A-Za-z]*.h) add_style_check_target(style "${LEAN_SOURCES}") add_test(NAME style_check COMMAND ${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py ${LEAN_SOURCES}) + +add_custom_target( + standard_lib ALL + COMMAND make LEAN=${CMAKE_BINARY_DIR}/shell/lean + DEPENDS ${CMAKE_BINARY_DIR}/shell/lean + WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard +)