feat(shell): add options --cpp and --discard

src/frontends/lean/parser.cpp

@@ -86,12 +86,14 @@ static name * g_tmp_prefix = nullptr;
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
-               snapshot const * s, snapshot_vector * sv, info_manager * im):
+               snapshot const * s, snapshot_vector * sv, info_manager * im,
+               bool keep_imported_proofs):
     m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name, s ? s->m_line : 1),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
+    m_keep_imported_thms = keep_imported_proofs;
     if (s) {
         m_local_level_decls  = s->m_lds;
         m_local_decls        = s->m_eds;
@@ -1279,7 +1281,8 @@ void parser::parse_imports() {
     unsigned num_threads = 0;
     if (get_parser_parallel_import(m_ios.get_options()))
         num_threads = m_num_threads;
-    m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads, true, m_ios);
+    m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads,
+                           m_keep_imported_thms, m_ios);
     for (auto const & f : lua_files) {
         std::string rname = find_file(f, {".lua"});
         system_import(rname.c_str());
@@ -1446,8 +1449,8 @@ void parser::save_type_info(expr const & e) {
 }
 
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions,
-                    unsigned num_threads, definition_cache * cache, declaration_index * index) {
+                    unsigned num_threads, definition_cache * cache, declaration_index * index, bool keep_thms) {
-    parser p(env, ios, in, strm_name, use_exceptions, num_threads);
+    parser p(env, ios, in, strm_name, use_exceptions, num_threads, nullptr, nullptr, nullptr, keep_thms);
     p.set_cache(cache);
     p.set_index(index);
     bool r = p();
@@ -1457,11 +1460,11 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c
 }
 
 bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
-                    definition_cache * cache, declaration_index * index) {
+                    definition_cache * cache, declaration_index * index, bool keep_thms) {
     std::ifstream in(fname);
     if (in.bad() || in.fail())
         throw exception(sstream() << "failed to open file '" << fname << "'");
-    return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index);
+    return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index, keep_thms);
 }
 
 void initialize_parser() {

src/frontends/lean/parser.h

@@ -120,6 +120,8 @@ class parser {
     // index support
     declaration_index *    m_index;
 
+    bool                   m_keep_imported_thms;
+
     // curr command token
     name                   m_cmd_token;
 
@@ -205,7 +207,7 @@ public:
            std::istream & strm, char const * str_name,
            bool use_exceptions = false, unsigned num_threads = 1,
            snapshot const * s = nullptr, snapshot_vector * sv = nullptr,
-           info_manager * im = nullptr);
+           info_manager * im = nullptr, bool keep_imported_proofs = true);
     ~parser();
 
     void set_cache(definition_cache * c) { m_cache = c; }
@@ -386,9 +388,9 @@ public:
 
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
                     bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr,
-                    declaration_index * index = nullptr);
+                    declaration_index * index = nullptr, bool keep_imported_proofs = true);
 bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
-                    definition_cache * cache = nullptr, declaration_index * index = nullptr);
+                    definition_cache * cache = nullptr, declaration_index * index = nullptr, bool keep_imported_proofs = true);
 
 void initialize_parser();
 void finalize_parser();

src/shell/lean.cpp

@@ -86,10 +86,12 @@ static void display_help(std::ostream & out) {
     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 << "  --output=file -o  save the final environment in binary format in the given file\n";
+    std::cout << "  --cpp=file -C     save the final environment as a C++ array\n";
     std::cout << "  --luahook=num -k  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";
     std::cout << "  --trust=num -t    trust level (default: 0) \n";
+    std::cout << "  --discard -T      discard the proof of imported theorems after checking\n";
     std::cout << "  --quiet -q        do not print verbose messages\n";
 #if defined(LEAN_MULTI_THREAD)
     std::cout << "  --server          start Lean in 'server' mode\n";
@@ -128,7 +130,9 @@ static struct option g_long_options[] = {
     {"luahook",     required_argument, 0, 'k'},
     {"githash",     no_argument,       0, 'g'},
     {"output",      required_argument, 0, 'o'},
+    {"cpp",         required_argument, 0, 'C'},
     {"trust",       required_argument, 0, 't'},
+    {"discard",     no_argument,       0, 'T'},
 #if defined(LEAN_MULTI_THREAD)
     {"server",      no_argument,       0, 'S'},
     {"threads",     required_argument, 0, 'j'},
@@ -144,7 +148,7 @@ static struct option g_long_options[] = {
     {0, 0, 0, 0}
 };
 
-#define BASIC_OPT_STR "FdD:qlupgvhk:012t:012o:c:i:"
+#define BASIC_OPT_STR "TFC:dD:qlupgvhk:012t:012o:c:i:"
 
 #if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD)
 static char const * g_opt_str = BASIC_OPT_STR "Sj:012s:012";
@@ -197,6 +201,23 @@ options set_config_option(options const & opts, char const * in) {
     }
 }
 
+static void export_as_cpp_file(std::string const & fname, char const * varname, environment const & env) {
+    std::ostringstream buffer(std::ofstream::binary);
+    export_module(buffer, env);
+    std::string r = buffer.str();
+    std::ofstream out(fname);
+    out << "// automatically generated file do not edit\n";
+    out << "namespace lean {\n";
+    out << "    char " << varname << "[" << r.size() + 1 << "] = {";
+    for (unsigned i = 0; i < r.size(); i++) {
+        if (i > 0)
+            out << ", ";
+        out << static_cast<unsigned>(static_cast<unsigned char>(r[i]));
+    }
+    out << "    }\n";
+    out << "}\n";
+}
+
 int main(int argc, char ** argv) {
     lean::initializer init;
     bool export_objects  = false;
@@ -206,8 +227,11 @@ int main(int argc, char ** argv) {
     unsigned num_threads = 1;
     bool use_cache       = false;
     bool gen_index       = false;
+    bool export_cpp      = false;
+    bool keep_thms       = true;
     options opts;
     std::string output;
+    std::string cpp_output;
     std::string cache_name;
     std::string index_name;
     input_kind default_k = input_kind::Lean; // default
@@ -250,6 +274,10 @@ int main(int argc, char ** argv) {
             output         = optarg;
             export_objects = true;
             break;
+        case 'C':
+            cpp_output = optarg;
+            export_cpp = true;
+            break;
         case 'c':
             cache_name = optarg;
             use_cache  = true;
@@ -260,6 +288,9 @@ int main(int argc, char ** argv) {
         case 't':
             trust_lvl = atoi(optarg);
             break;
+        case 'T':
+            keep_thms = false;
+            break;
         case 'q':
             opts = opts.update("verbose", false);
             break;
@@ -324,7 +355,8 @@ int main(int argc, char ** argv) {
                     if (only_deps) {
                         if (!display_deps(env, std::cout, std::cerr, argv[i]))
                             ok = false;
-                    } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr, index_ptr)) {
+                    } else if (!parse_commands(env, ios, argv[i], false, num_threads,
+                                               cache_ptr, index_ptr, keep_thms)) {
                         ok = false;
                     }
                 } else if (k == input_kind::Lua) {
@@ -358,6 +390,9 @@ int main(int argc, char ** argv) {
             std::ofstream out(output, std::ofstream::binary);
             export_module(out, env);
         }
+        if (export_cpp && ok) {
+            export_as_cpp_file(cpp_output, "olean_lib", env);
+        }
         return ok ? 0 : 1;
     } catch (lean::exception & ex) {
         lean::display_error(diagnostic(env, ios), nullptr, ex);