feat(shell): add '--hott' command line option

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

library/hott/logic.lean

@@ -0,0 +1,2 @@
+definition id.{l} (A : Type.{l}) (a : A) : A := a
+check ∀ x : Type.{0}, x

library/standard/logic.lean

@@ -0,0 +1,2 @@
+definition [inline] Bool : Type.{0} := Type.{1}
+

src/shell/lean.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
 #include "kernel/standard/standard.h"
+#include "kernel/hott/hott.h"
 #include "library/module.h"
 #include "library/io_state_stream.h"
 #include "library/error_handling/error_handling.h"
@@ -36,6 +37,7 @@ using lean::io_state;
 using lean::io_state_stream;
 using lean::regular;
 using lean::mk_environment;
+using lean::mk_hott_environment;
 
 enum class input_kind { Unspecified, Lean, Lua };
 
@@ -65,6 +67,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --trust=num -t    trust level (default: 0) \n";
     std::cout << "  --quiet -q        do not print verbose messages\n";
     std::cout << "  --interactive -i  read blocks of commands from the input stream\n";
+    std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -96,6 +99,7 @@ static struct option g_long_options[] = {
     {"trust",       required_argument, 0, 't'},
     {"interactive", no_argument,       0, 'i'},
     {"quiet",       no_argument,       0, 'q'},
+    {"hott",        no_argument,       0, 'H'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",      required_argument, 0, 's'},
 #endif
@@ -103,11 +107,13 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "iqlupgvhc:012s:012t:012o:";
+static char const * g_opt_str = "Hiqlupgvhc:012s:012t:012o:";
 #else
-static char const * g_opt_str = "iqlupgvhc:012t:012o:";
+static char const * g_opt_str = "Hiqlupgvhc:012t:012o:";
 #endif
 
+enum class lean_mode { Standard, HoTT };
+
 int main(int argc, char ** argv) {
     lean::save_stack_info();
     lean::register_modules();
@@ -115,6 +121,7 @@ int main(int argc, char ** argv) {
     unsigned trust_lvl  = 0;
     bool quiet          = false;
     bool interactive    = false;
+    lean_mode mode      = lean_mode::Standard;
     std::string output;
     input_kind default_k = input_kind::Lean; // default
     while (true) {
@@ -122,6 +129,10 @@ int main(int argc, char ** argv) {
         if (c == -1)
             break; // end of command line
         switch (c) {
+        case 'H':
+            mode = lean_mode::HoTT;
+            lean::init_lean_path("hott");
+            break;
         case 'i':
             interactive = true;
             break;
@@ -166,7 +177,7 @@ int main(int argc, char ** argv) {
         }
     }
 
-    environment env = mk_environment(trust_lvl);
+    environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl);
     io_state ios(lean::mk_simple_formatter());
     if (quiet)
         ios.set_option("verbose", false);

src/util/lean_path.cpp

@@ -128,14 +128,13 @@ std::string get_path(std::string f) {
 
 static std::string              g_lean_path;
 static std::vector<std::string> g_lean_path_vector;
-struct init_lean_path {
-    init_lean_path() {
+void init_lean_path(char const * kernel_instance_name) {
     char * r = getenv("LEAN_PATH");
     if (r == nullptr) {
         g_lean_path  = ".";
         std::string exe_path = get_path(get_exe_location());
         g_lean_path += g_path_sep;
-            g_lean_path += exe_path + g_sep + ".." + g_sep + "library";
+        g_lean_path += exe_path + g_sep + ".." + g_sep + "library" + g_sep + kernel_instance_name;
         g_lean_path += g_path_sep;
         g_lean_path += exe_path;
     } else {
@@ -154,9 +153,12 @@ struct init_lean_path {
     }
     if (j > i)
         g_lean_path_vector.push_back(g_lean_path.substr(i, j - i));
-    }
+}
+
+struct init_lean_path_fn {
+    init_lean_path_fn() { init_lean_path("standard"); }
 };
-static init_lean_path g_init_lean_path;
+static init_lean_path_fn g_init_lean_path_fn;
 static std::string       g_sep_str(1, g_sep);
 
 bool has_file_ext(std::string const & fname, char const * ext) {

src/util/lean_path.h

@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/name.h"
 namespace lean {
-/**
-   \brief Return the LEAN_PATH string
-*/
+/** \brief Initialize the lean_path for the given kernel instance */
+void init_lean_path(char const * kernel_instance_name);
+/** \brief Return the LEAN_PATH string */
 char const * get_lean_path();
 /**
    \brief Search the file \c fname in the LEAN_PATH. Throw an