From 795359ee49611cb0e8b0a10848a901bf2dad510b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 3 Sep 2019 14:34:57 +0200
Subject: [PATCH] feat(shell/lean): re-add --run flag

---
 src/library/compiler/ir_interpreter.cpp |  4 ++--
 src/shell/lean.cpp                      | 13 +++++++++++--
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index 90a8f96e84..737623fb24 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -529,8 +529,6 @@ public:
     uint32 run_main(int argc, char * argv[]) {
         decl d = get_fdecl("main");
         array_ref<param> const & params = decl_params(d);
-        object * w = io_mk_world();
-        m_arg_stack.push_back(w);
         if (params.size() == 2) {
             lean_object * in = lean_box(0);
             int i = argc;
@@ -545,6 +543,8 @@ public:
         } else {
             lean_assert(params.size() == 1);
         }
+        object * w = io_mk_world();
+        m_arg_stack.push_back(w);
         push_frame("main", 0);
         w = eval_body(decl_fun_body(d));
         pop_frame();
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index a7e894bf5e..b090075d0b 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -43,6 +43,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "init/init.h"
 #include "frontends/lean/simple_pos_info_provider.h"
+#include "library/compiler/ir_interpreter.h"
 #ifdef _MSC_VER
 #include <io.h>
 #define STDOUT_FILENO 1
@@ -219,6 +220,7 @@ static struct option g_long_options[] = {
     {"version",      no_argument,       0, 'v'},
     {"help",         no_argument,       0, 'h'},
     {"githash",      no_argument,       0, 'g'},
+    {"run",          no_argument,       0, 'r'},
     {"make",         no_argument,       0, 'm'},
     {"stdin",        no_argument,       0, 'i'},
     {"memory",       required_argument, 0, 'M'},
@@ -346,6 +348,7 @@ int main(int argc, char ** argv) {
     auto init_start = std::chrono::steady_clock::now();
     ::initializer init;
     second_duration init_time = std::chrono::steady_clock::now() - init_start;
+    bool run = false;
     bool make_mode = false;
     bool use_stdin = false;
     unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1;
@@ -402,6 +405,9 @@ int main(int argc, char ** argv) {
             case 'i':
                 use_stdin = true;
                 break;
+            case 'r':
+                run = true;
+                break;
             case 'm':
                 make_mode = true;
                 break;
@@ -496,12 +502,12 @@ int main(int argc, char ** argv) {
         contents = buf.str();
         main_module_name = name("_stdin");
     } else {
-        if (argc - optind != 1) {
+        if (!run && argc - optind != 1) {
             std::cerr << "Expected exactly one file name\n";
             display_help(std::cerr);
             return 1;
         }
-        mod_fn = lrealpath(argv[optind]);
+        mod_fn = lrealpath(argv[optind++]);
         contents = read_file(mod_fn);
         main_module_name = module_name_of_file2(mod_fn);
     }
@@ -567,6 +573,9 @@ int main(int argc, char ** argv) {
             env.display_stats();
         }
 
+        if (run && ok) {
+            return ir::run_main(env, argc - optind, argv + optind);
+        }
         if (make_mode && ok) {
             auto olean_fn = olean_of_lean(mod_fn);
             time_task t(".olean serialization",