feat(util/lean_path): add function for searching for a file in the LEAN_PATH

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/util/lean_path.cpp

@@ -6,12 +6,17 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <cstdlib>
+#include <fstream>
+#include <vector>
 #include "util/exception.h"
+#include "util/sstream.h"
 
 namespace lean {
 #if defined(LEAN_WINDOWS)
 // Windows version
 #include <windows.h>
+static char g_path_sep = ';';
+static char g_sep      = '\\';
 static std::string get_exe_location() {
     HMODULE hModule = GetModuleHandleW(NULL);
     WCHAR path[MAX_PATH];
@@ -22,6 +27,8 @@ static std::string get_exe_location() {
 // OSX version
 #include <mach-o/dyld.h>
 #include <limits.h>
+static char g_path_sep = ':';
+static char g_sep      = '/';
 static std::string get_exe_location() {
     char buf[PATH_MAX];
     uint32_t bufsize = PATH_MAX;
@@ -36,6 +43,8 @@ static std::string get_exe_location() {
 #include <sys/stat.h>
 #include <limits.h> // NOLINT
 #include <stdio.h>
+static char g_path_sep = ':';
+static char g_sep      = '/';
 static std::string get_exe_location() {
     char path[PATH_MAX];
     char dest[PATH_MAX];
@@ -48,17 +57,42 @@ static std::string get_exe_location() {
     }
 }
 #endif
-static std::string g_lean_path;
+static std::string              g_lean_path;
+static std::vector<std::string> g_lean_path_vector;
 struct init_lean_path {
     init_lean_path() {
         char * r = getenv("LEAN_PATH");
-        if (r == nullptr)
-            g_lean_path = get_exe_location();
-        else
+        if (r == nullptr) {
+            g_lean_path  = ".";
+            g_lean_path += g_path_sep;
+            g_lean_path += get_exe_location();
+        } else {
             g_lean_path = r;
+        }
+        unsigned i  = 0;
+        unsigned j  = 0;
+        unsigned sz = g_lean_path.size();
+        for (; j < sz; j++) {
+            if (g_lean_path[j] == g_path_sep) {
+                if (j > i)
+                    g_lean_path_vector.push_back(g_lean_path.substr(i, j - i));
+                i = j + 1;
+            }
+        }
     }
 };
 static init_lean_path g_init_lean_path;
+
+std::string find_file(char const * fname) {
+    for (auto path : g_lean_path_vector) {
+        auto file = path + g_sep + fname;
+        std::ifstream ifile(file);
+        if (ifile)
+            return file;
+    }
+    throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH");
+}
+
 char const * get_lean_path() {
     return g_lean_path.c_str();
 }

src/util/lean_path.h

@@ -5,6 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 namespace lean {
+/**
+   \brief Return the LEAN_PATH string
+*/
 char const * get_lean_path();
+/**
+   \brief Search the file \c fname in the LEAN_PATH. Throw an
+   exception if the file was not found.
+*/
+std::string find_file(char const * fname);
 }