From 777582380f9e4cd7f33c5e210132038458453425 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Dec 2013 17:56:53 -0800 Subject: [PATCH] feat(util/lean_path): add support for LEAN_PATH Signed-off-by: Leonardo de Moura --- src/shell/CMakeLists.txt | 2 ++ src/shell/lean.cpp | 8 ++++- src/util/CMakeLists.txt | 2 +- src/util/{exe_location.cpp => lean_path.cpp} | 31 ++++++++++++-------- src/util/{exe_location.h => lean_path.h} | 2 +- 5 files changed, 30 insertions(+), 15 deletions(-) rename src/util/{exe_location.cpp => lean_path.cpp} (65%) rename src/util/{exe_location.h => lean_path.h} (85%) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a131406de..a8cda4323 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -13,6 +13,8 @@ add_test(lean_version1 ${CMAKE_CURRENT_BINARY_DIR}/lean --version) add_test(lean_version2 ${CMAKE_CURRENT_BINARY_DIR}/lean --v) add_test(lean_ghash1 ${CMAKE_CURRENT_BINARY_DIR}/lean -g) add_test(lean_ghash2 ${CMAKE_CURRENT_BINARY_DIR}/lean --githash) +add_test(lean_path1 ${CMAKE_CURRENT_BINARY_DIR}/lean -p) +add_test(lean_path2 ${CMAKE_CURRENT_BINARY_DIR}/lean --path) add_test(lean_luahook1 ${CMAKE_CURRENT_BINARY_DIR}/lean --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") add_test(lean_luahook2 ${CMAKE_CURRENT_BINARY_DIR}/lean -c 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index ddd40f3d7..93b708d90 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "util/script_state.h" #include "util/thread.h" +#include "util/lean_path.h" #include "kernel/printer.h" #include "kernel/environment.h" #include "library/io_state.h" @@ -55,6 +56,7 @@ static void display_help(std::ostream & out) { std::cout << " --help -h display this message\n"; std::cout << " --version -v display version number\n"; std::cout << " --githash display the git commit hash number used to build this binary\n"; + std::cout << " --path display the path used for finding Lean libraries and extensions\n"; std::cout << " --luahook=num -c how often the Lua interpreter checks the interrupted flag,\n"; std::cout << " it is useful for interrupting non-terminating user scripts,\n"; std::cout << " 0 means 'do not check'.\n"; @@ -82,6 +84,7 @@ static struct option g_long_options[] = { {"help", no_argument, 0, 'h'}, {"lean", no_argument, 0, 'l'}, {"lua", no_argument, 0, 'u'}, + {"path", no_argument, 0, 'p'}, {"luahook", required_argument, 0, 'c'}, {"githash", no_argument, 0, 'g'}, #if defined(LEAN_USE_BOOST) @@ -95,7 +98,7 @@ int main(int argc, char ** argv) { lean::register_modules(); input_kind default_k = input_kind::Lean; // default while (true) { - int c = getopt_long(argc, argv, "lugvhc:012s:012", g_long_options, NULL); + int c = getopt_long(argc, argv, "lupgvhc:012s:012", g_long_options, NULL); if (c == -1) break; // end of command line switch (c) { @@ -117,6 +120,9 @@ int main(int argc, char ** argv) { case 'c': script_state::set_check_interrupt_freq(atoi(optarg)); break; + case 'p': + std::cout << lean::get_lean_path() << "\n"; + return 0; case 's': lean::set_thread_stack_size(atoi(optarg)*1024); break; diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 1f60ad9b5..270052e50 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -8,6 +8,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp script_state.cpp script_exception.cpp splay_map.cpp lua.cpp - luaref.cpp stackinfo.cpp exe_location.cpp ${THREAD_CPP}) + luaref.cpp stackinfo.cpp lean_path.cpp ${THREAD_CPP}) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/exe_location.cpp b/src/util/lean_path.cpp similarity index 65% rename from src/util/exe_location.cpp rename to src/util/lean_path.cpp index 7d2989ec4..07cd6e1a6 100644 --- a/src/util/exe_location.cpp +++ b/src/util/lean_path.cpp @@ -5,29 +5,29 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/exception.h" namespace lean { -static std::string g_exe_location; #if defined(LEAN_WINDOWS) // Windows version #include -static void init_exe_location() { +static std::string get_exe_location() { HMODULE hModule = GetModuleHandleW(NULL); WCHAR path[MAX_PATH]; GetModuleFileNameW(hModule, path, MAX_PATH); - g_exe_location = path; + return std::string(path); } #elif defined(__APPLE__) // OSX version #include #include -static void init_exe_location() { +static std::string get_exe_location() { char buf[PATH_MAX]; uint32_t bufsize = PATH_MAX; if (_NSGetExecutablePath(buf, &bufsize) != 0) throw exception("failed to locate Lean executable location"); - g_exe_location = buf; + return std::string(buf); } #else // Linux version @@ -36,7 +36,7 @@ static void init_exe_location() { #include #include // NOLINT #include -static void init_exe_location() { +static std::string get_exe_location() { char path[PATH_MAX]; char dest[PATH_MAX]; pid_t pid = getpid(); @@ -44,15 +44,22 @@ static void init_exe_location() { if (readlink(path, dest, PATH_MAX) == -1) { throw exception("failed to locate Lean executable location"); } else { - g_exe_location = dest; + return std::string(dest); } } #endif -struct init_exe_location_proc { - init_exe_location_proc() { init_exe_location(); } +static std::string g_lean_path; +struct init_lean_path { + init_lean_path() { + char * r = getenv("LEAN_PATH"); + if (r == nullptr) + g_lean_path = get_exe_location(); + else + g_lean_path = r; + } }; -static init_exe_location_proc g_init_exe_location_proc; -char const * get_exe_location() { - return g_exe_location.c_str(); +static init_lean_path g_init_lean_path; +char const * get_lean_path() { + return g_lean_path.c_str(); } } diff --git a/src/util/exe_location.h b/src/util/lean_path.h similarity index 85% rename from src/util/exe_location.h rename to src/util/lean_path.h index 6b5754880..6bfb99418 100644 --- a/src/util/exe_location.h +++ b/src/util/lean_path.h @@ -6,5 +6,5 @@ Author: Leonardo de Moura */ #pragma once namespace lean { -char const * get_exe_location(); +char const * get_lean_path(); }