feat: lean --src-deps

Author: tydeu

src/Lean/Elab/Import.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Module
-import Lean.Data.Json
+import Lean.Util.Paths
 
 namespace Lean.Elab
 
@@ -42,4 +42,12 @@ def printImports (input : String) (fileName : Option String) : IO Unit := do
     let fname ← findOLean dep.module
     IO.println fname
 
+@[export lean_print_import_srcs]
+def printImportSrcs (input : String) (fileName : Option String) : IO Unit := do
+  let sp ← initSrcSearchPath
+  let (deps, _, _) ← parseImports input fileName
+  for dep in deps do
+    let fname ← findLean sp dep.module
+    IO.println fname
+
 end Lean.Elab

src/Lean/Util/Path.lean

@@ -104,17 +104,26 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit :
 private def initSearchPathInternal : IO Unit := do
   initSearchPath (← getBuildDir)
 
+/-- Find the compiled `.olean` of a module in the `LEAN_PATH` search path. -/
 partial def findOLean (mod : Name) : IO FilePath := do
   let sp ← searchPathRef.get
   if let some fname ← sp.findWithExt "olean" mod then
     return fname
   else
     let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
-    let mut msg := s!"unknown module prefix '{pkg}'
+    throw <| IO.userError s!"unknown module prefix '{pkg}'\n\n\
+      No directory '{pkg}' or file '{pkg}.olean' in the search path entries:\n\
+      {"\n".intercalate <| sp.map (·.toString)}"
 
-No directory '{pkg}' or file '{pkg}.olean' in the search path entries:
-{"\n".intercalate <| sp.map (·.toString)}"
-    throw <| IO.userError msg
+/-- Find the `.lean` source of a module in a `LEAN_SRC_PATH` search path. -/
+partial def findLean (sp : SearchPath) (mod : Name) : IO FilePath := do
+  if let some fname ← sp.findWithExt "lean" mod then
+    return fname
+  else
+    let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
+    throw <| IO.userError s!"unknown module prefix '{pkg}'\n\n\
+      No directory '{pkg}' or file '{pkg}.lean' in the search path entries:\n\
+      {"\n".intercalate <| sp.map (·.toString)}"
 
 /-- Infer module name of source file name. -/
 @[export lean_module_name_of_file]

src/util/shell.cpp

@@ -225,6 +225,7 @@ static void display_help(std::ostream & out) {
     std::cout << "      --json             report Lean output (e.g., messages) as JSON (one per line)\n";
     std::cout << "  -E  --error=kind       report Lean messages of kind as errors\n";
     std::cout << "      --deps             just print dependencies of a Lean input\n";
+    std::cout << "      --src-deps         just print dependency sources of a Lean input\n";
     std::cout << "      --print-prefix     print the installation prefix for Lean and exit\n";
     std::cout << "      --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
     std::cout << "      --profile          display elaboration/type checking time for each definition/theorem\n";
@@ -235,6 +236,7 @@ static void display_help(std::ostream & out) {
     std::cout << "      -D name=value      set a configuration option (see set_option command)\n";
 }
 
+static int only_src_deps = 0;
 static int print_prefix = 0;
 static int print_libdir = 0;
 static int json_output = 0;
@@ -255,6 +257,7 @@ static struct option g_long_options[] = {
     {"stats",        no_argument,       0, 'a'},
     {"quiet",        no_argument,       0, 'q'},
     {"deps",         no_argument,       0, 'd'},
+    {"src-deps",     no_argument,       &only_src_deps, 1},
     {"deps-json",    no_argument,       0, 'J'},
     {"timeout",      optional_argument, 0, 'T'},
     {"c",            optional_argument, 0, 'c'},
@@ -399,6 +402,12 @@ void print_imports(std::string const & input, std::string const & fname) {
     consume_io_result(lean_print_imports(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
 }
 
+/* def printImportSrcs (input : String) (fileName : Option String := none) : IO Unit */
+extern "C" object* lean_print_import_srcs(object* input, object* file_name, object* w);
+void print_import_srcs(std::string const & input, std::string const & fname) {
+    consume_io_result(lean_print_import_srcs(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
+}
+
 /* def printImportsJson (fileNames : Array String) : IO Unit */
 extern "C" object* lean_print_imports_json(object * file_names, object * w);
 void print_imports_json(array_ref<string_ref> const & fnames) {
@@ -697,6 +706,11 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
             return 0;
         }
 
+        if (only_src_deps) {
+            print_import_srcs(contents, mod_fn);
+            return 0;
+        }
+
         // Quick and dirty `#lang` support
         // TODO: make it extensible, and add `lean4md`
         if (contents.compare(0, 5, "#lang") == 0) {