feat: infer module name from cwd instead of LEAN_PATH, also make build system less specific to Init/

.gitignore

@@ -24,4 +24,4 @@ settings.json
 *.produced.out
 CMakeSettings.json
 CppProperties.json
-/src/Init/Makefile
+/src/Makefile

src/CMakeLists.txt

@@ -489,7 +489,7 @@ configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
 configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h")
 install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}")
 if(NOT STAGE0)
-  configure_file("${LEAN_SOURCE_DIR}/Init/Makefile.in" "${LEAN_SOURCE_DIR}/Init/Makefile")
+  configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile")
 endif()
 
 include_directories("${LEAN_BINARY_DIR}")
@@ -618,7 +618,7 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma
 endif()
 
 add_custom_target(clean-stdlib
-  WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init"
+  WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
   COMMAND find . -name '*.olean' -delete
   COMMAND find . -name '*.depend' -delete
   COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
@@ -627,7 +627,7 @@ add_custom_target(clean-stdlib
 add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
-install(DIRECTORY "${CMAKE_SOURCE_DIR}/Init" DESTINATION "${LIBRARY_DIR}"
+install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}"
         FILES_MATCHING
         PATTERN "*.lean"
         PATTERN "*.olean"

src/Init/Lean/Util/Path.lean

@@ -110,23 +110,24 @@ match results with
 | []    => pure none
    | _     => throw (IO.userError ("file '" ++ fname ++ "' is contained in multiple packages: " ++ ", ".intercalate (results.map Prod.fst)))
 
+/-- Infer module name of source file name, assuming that `lean` is called from the package source root. -/
 @[export lean_module_name_of_file]
-def moduleNameOfFileName (fname : String) : IO (Option Name) := do
-some (pkg, path) ← findAtSearchPath fname
-  | pure none;
+def moduleNameOfFileName (fname : String) : IO Name := do
 fname ← realPathNormalized fname;
-let fnameSuffix := fname.drop path.length;
+root ← IO.currentDir >>= realPathNormalized;
+when (!root.isPrefixOf fname) $
+  throw $ IO.userError $ "input file '" ++ fname ++ "' must be contained in current directory (" ++ root ++ ")";
+let fnameSuffix := fname.drop root.length;
 let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
 some extPos ← pure (fnameSuffix.revPosOf '.')
-  | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing"));
+  | throw (IO.userError ("failed to convert file name '" ++ fname ++ "' to module name, extension is missing"));
 let modNameStr := fnameSuffix.extract 0 extPos;
 let extStr     := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize;
 let parts      := modNameStr.splitOn pathSep;
-let modName    := parts.foldl mkNameStr pkg;
+let modName    := parts.foldl mkNameStr Name.anonymous;
 pure modName
 
 -- normalize `A` to `A.Default`
-@[export lean_normalize_module_name]
 def normalizeModuleName : Name → Name
 | Name.str Name.anonymous pkg _ => mkNameSimple pkg ++ "Default"
 | m                             => m

src/Makefile.in

@@ -1,8 +1,8 @@
 # Copyright (c) 2018 Simon Hudon. All rights reserved.
 # Released under Apache 2.0 license as described in the file LICENSE.
 # Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
-LEAN ?= ../../bin/lean
-LEANC ?= ../../bin/leanc
+LEAN ?= ../bin/lean
+LEANC ?= ../bin/leanc
 LEAN_ROOT ?= .
 # Even though we copy the sources into a new directory for stage2/3, we
 # read the list of files to compile from the original directory to avoid
@@ -10,14 +10,14 @@ LEAN_ROOT ?= .
 SRCS = $(shell cd $(LEAN_ROOT); find . -name '*.lean')
 DEPS = $(addprefix $(LEAN_ROOT)/,$(SRCS:.lean=.depend))
 OPTS = @LEAN_EXTRA_MAKE_OPTS@
-STAGE0_DIR = ../../stage0
+STAGE0_DIR = ../stage0
 C_OUT ?= .
 ifndef OUT
 $(error "`OUT` must be set (use cmake)")
 endif
 OBJS = $(SRCS:.lean=.olean)
 # ensure deterministic ordering
-CS_CORE=$(addprefix Init/,$(sort $(SRCS:.lean=.c)))
+CS_CORE=$(sort $(SRCS:.lean=.c))
 
 SHELL = /usr/bin/env bash -eo pipefail
 
@@ -55,10 +55,10 @@ $(OUT)/libleanstdlib.a: $(addprefix $(OUT)/,$(SRCS:.lean=.o))
 update-stage0:
 	-rm -r $(STAGE0_DIR)
 	-mkdir -p $(STAGE0_DIR)/stdlib
-	for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/Init/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/Init/$$f; done
+	for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
 	echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt
 # don't copy untracked crap
-	cd ..; git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'
+	git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'
 	-git add $(STAGE0_DIR)
 
 .PRECIOUS: %.depend $(C_OUT)/%.c

src/frontends/lean/parser.cpp

@@ -2158,12 +2158,6 @@ void parser::parse_new_frontend_cmd() {
 #endif
 
 
-extern "C" object* lean_normalize_module_name(object* m);
-
-name normalize_module_name(name m) {
-    return name(lean_normalize_module_name(m.to_obj_arg()));
-}
-
 void parser::process_imports() {
     // we assume the Lean parser has already imported the modules into `m_env`
 

src/shell/CMakeLists.txt

@@ -11,16 +11,16 @@ if(NOT STAGE0)
   set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
 
   add_custom_target(make_stdlib
-    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init"
-    COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=." $(MAKE) "${CMAKE_BINARY_DIR}/stage1/Init/libleanstdlib.a"
+    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
+    COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
       "LEAN=$<TARGET_FILE:lean_stage0>"
       "LEANC_OPTS=${LEANC_OPTS}"
-      "OUT=${CMAKE_BINARY_DIR}/stage1/Init"
+      "OUT=${CMAKE_BINARY_DIR}/stage1"
       # share .c files between different build configurations
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1/Init"
+      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
     DEPENDS stage0)
   set_target_properties(leanstdlib PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/Init/libleanstdlib.a"
+    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
     IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
   add_dependencies(leanstdlib make_stdlib)
   install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
@@ -28,11 +28,11 @@ if(NOT STAGE0)
   set(PREV_LEAN "$<TARGET_FILE:lean>")
   foreach(STAGE RANGE 2 3)
     add_custom_target(make_stdlib_stage${STAGE}
-      COMMAND cd "${LEAN_SOURCE_DIR}/Init" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/Init/'{}' '\;'
-      COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}/Init" && LEAN_PATH=Init=. $(MAKE) ./libleanstdlib.a
+      COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;'
+      COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a
         "LEAN=${PREV_LEAN}"
         "LEANC=${LEAN_SOURCE_DIR}/../bin/leanc"
-        "LEAN_ROOT=${LEAN_SOURCE_DIR}/Init"
+        "LEAN_ROOT=${LEAN_SOURCE_DIR}"
         "LEANC_OPTS=${LEANC_OPTS}"
         "OUT=."
         # recreate everything if the previous compiler has changed
@@ -40,7 +40,7 @@ if(NOT STAGE0)
     )
     add_library(leanstdlib_stage${STAGE} STATIC IMPORTED)
     set_target_properties(leanstdlib_stage${STAGE} PROPERTIES
-      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/Init/libleanstdlib.a"
+      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a"
       IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
     add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE})
     add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp)
@@ -54,10 +54,10 @@ if(NOT STAGE0)
 
   add_custom_target(update-stage0
     COMMAND make update-stage0
-      "OUT=${CMAKE_BINARY_DIR}/stage1/Init"
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1/Init"
+      "OUT=${CMAKE_BINARY_DIR}/stage1"
+      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
     DEPENDS leanstdlib
-    WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/Init")
+    WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
 endif()
 
 add_executable(lean lean.cpp)

src/shell/lean.cpp

@@ -304,7 +304,7 @@ void load_plugin(std::string path) {
     // we never want to look up plugins using the system library search
     path = lrealpath(path);
     std::string pkg = stem(path);
-    std::string sym = "initialize_" + pkg + "_Default";
+    std::string sym = "initialize_" + pkg;
 #ifdef LEAN_WINDOWS
     HMODULE h = LoadLibrary(path.c_str());
     if (!h) {
@@ -354,8 +354,13 @@ void init_search_path() {
 }
 
 extern "C" object* lean_module_name_of_file(object* fname, object* w);
-optional<name> module_name_of_file(std::string const & fname) {
-    return get_io_result<option_ref<name>>(lean_module_name_of_file(mk_string(fname), io_mk_world())).get();
+optional<name> module_name_of_file(std::string const & fname, bool optional) {
+    object * o = lean_module_name_of_file(mk_string(fname), io_mk_world());
+    if (io_result_is_error(o) && optional) {
+        return lean::optional<name>();
+    } else {
+        return some(get_io_result<name>(o));
+    }
 }
 
 /* def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) */
@@ -597,7 +602,7 @@ int main(int argc, char ** argv) {
             }
             mod_fn = lrealpath(argv[optind++]);
             contents = read_file(mod_fn);
-            main_module_name = module_name_of_file(mod_fn);
+            main_module_name = module_name_of_file(mod_fn, /* optional */ !olean_fn && !c_output);
         }
 
         bool ok = true;
@@ -682,10 +687,6 @@ int main(int argc, char ** argv) {
         }
 
         if (c_output && ok) {
-            if (!main_module_name) {
-                std::cerr << "cannot extract code, module name of input file is not known\n";
-                return 1;
-            }
             std::ofstream out(*c_output);
             if (out.fail()) {
                 std::cerr << "failed to create '" << *c_output << "'\n";

tests/plugin/Default.lean.expected.out

@@ -1 +0,0 @@
-Default.lean:5:4: error: SNAKES!!

tests/plugin/SnakeLinter.lean.expected.out

@@ -0,0 +1 @@
+SnakeLinter.lean:5:4: error: SNAKES!!

tests/plugin/test_single.sh

@@ -5,7 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then
 fi
 ulimit -s 8192
 BIN_DIR=../../bin
-export LEAN_PATH=Init=../../src/Init:Test=.
+export LEAN_PATH=Init=../../src/Init
 if [ $# -ne 2 ]; then
     INTERACTIVE=no
 else
@@ -31,14 +31,13 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
-# NOTE: out name has to match package name in LEAN_PATH above
-$BIN_DIR/leanc -O3 -DNDEBUG -shared -o "Test.so" $ff.c
+$BIN_DIR/leanc -O3 -DNDEBUG -shared -o "${ff%.lean}.so" "$ff.c"
 if [ $? -ne 0 ]; then
     echo "Failed to compile C file $ff.c"
     exit 1
 fi
 
-$BIN_DIR/lean --plugin="Test.so" "$ff" 2>&1 | sed "s|^$ff|$f|" > "$f.produced.out"
+$BIN_DIR/lean --plugin="${ff%.lean}.so" "$ff" 2>&1 | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"