feat(shell/lean): add '-o' command line option

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

src/frontends/lean/builtin_cmds.cpp

@@ -37,7 +37,7 @@ environment universe_cmd(parser & p) {
     } else {
         name const & ns = get_namespace(env);
         name full_n  = ns + n;
-        env = env.add_universe(full_n);
+        env = module::add_universe(env, full_n);
         if (!ns.is_anonymous())
             env = add_alias(env, n, mk_global_univ(full_n));
     }
@@ -115,9 +115,9 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
         name const & ns = get_namespace(env);
         name full_n  = ns + n;
         if (is_axiom)
-            env = env.add(check(env, mk_axiom(full_n, ls, type)));
+            env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
         else
-            env = env.add(check(env, mk_var_decl(full_n, ls, type)));
+            env = module::add(env, check(env, mk_var_decl(full_n, ls, type)));
         if (!ns.is_anonymous())
             env = add_alias(env, n, mk_constant(full_n));
         return env;
@@ -238,12 +238,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
         auto type_value = p.elaborate(type, value, ls);
         type  = type_value.first;
         value = type_value.second;
-        env = env.add(check(env, mk_theorem(real_n, ls, type, value)));
+        env = module::add(env, check(env, mk_theorem(real_n, ls, type, value)));
     } else {
         auto type_value = p.elaborate(type, value, ls);
         type  = type_value.first;
         value = type_value.second;
-        env = env.add(check(env, mk_definition(env, real_n, ls, type, value, is_opaque)));
+        env = module::add(env, check(env, mk_definition(env, real_n, ls, type, value, is_opaque)));
     }
     return env;
 }

src/shell/CMakeLists.txt

@@ -6,6 +6,7 @@ install(TARGETS lean DESTINATION bin)
 # add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
 # add_test(example1_stdin2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "-l" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
 # add_test(example1_stdin3 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "--lean" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
+# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
 add_test(lean_help1 ${CMAKE_CURRENT_BINARY_DIR}/lean --help)
 add_test(lean_help2 ${CMAKE_CURRENT_BINARY_DIR}/lean --h)
 add_test(lean_version1 ${CMAKE_CURRENT_BINARY_DIR}/lean --version)
@@ -48,15 +49,6 @@ FOREACH(T ${LEANRUNTESTS})
            COMMAND "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)
 
-# # LEAN INTERACTIVE TESTS
-# file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
-# FOREACH(T ${LEANINTERACTIVETESTS})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leaninteractivetest_${T_NAME}"
-#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
-#            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
-# ENDFOREACH(T)
-
 # # LEAN SLOW TESTS
 # file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
 # FOREACH(T ${LEANSLOWTESTS})

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 "library/module.h"
 #include "library/io_state_stream.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
@@ -27,7 +28,6 @@ Author: Leonardo de Moura
 #include "kernel/io_state.h"
 #include "library/printer.h"
 #include "library/kernel_bindings.h"
-
 #include "frontends/lean/shell.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/register_module.h"
@@ -126,7 +126,7 @@ static char const * g_opt_str = "qlupgvhc:012t:012o:";
 int main(int argc, char ** argv) {
     lean::save_stack_info();
     lean::register_modules();
-    // bool export_objects = false;
+    bool export_objects = false;
     unsigned trust_lvl  = 0;
     bool quiet          = false;
     std::string output;
@@ -165,7 +165,7 @@ int main(int argc, char ** argv) {
             break;
         case 'o':
             output = optarg;
-            // export_objects = true;
+            export_objects = true;
             break;
         case 't':
             trust_lvl = atoi(optarg);
@@ -247,8 +247,10 @@ int main(int argc, char ** argv) {
                     lean_unreachable(); // LCOV_EXCL_LINE
                 }
             }
-            // if (export_objects)
+            if (export_objects) {
-            //    env->export_objects(output);
+                std::ofstream out(output, std::ofstream::binary);
+                export_module(out, env);
+            }
             return ok ? 0 : 1;
         }
     } catch (lean::exception & ex) {

tests/lean/run/simple.lean

@@ -0,0 +1,23 @@
+section
+  parameter A : Type
+
+  definition eq (a b : A) : Bool
+  := ∀P : A → Bool, P a → P b
+
+  theorem subst (P : A → Bool) (a b : A) (H1 : eq a b) (H2 : P a) : P b
+  := H1 P H2
+
+  theorem refl (a : A) : eq a a
+  := λ (P : A → Bool) (H : P a), H
+
+  theorem symm (a b : A) (H : eq a b) : eq b a
+  := subst (λ x : A, eq x a) a b H (refl a)
+
+  theorem trans (a b c : A) (H1 : eq a b) (H2 : eq b c) : eq a c
+  := subst (λ x : A, eq a x) b c H2 H1
+end
+
+check subst.{1}
+check refl.{1}
+check symm.{1}
+check trans.{1}