feat(frontends/lean): check modification time of imported files

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

src/frontends/lean/server.cpp

@@ -187,6 +187,8 @@ server::worker::worker(environment const & env, io_state const & ios, definition
                     unsigned i = todo_file->find(todo_line_num);
                     todo_file->m_snapshots.resize(i);
                     s = i == 0 ? m_empty_snapshot : todo_file->m_snapshots[i-1];
+                    if (direct_imports_have_changed(s.m_env))
+                        s = m_empty_snapshot;
                     lean_assert(s.m_line > 0);
                     todo_file->m_info.start_from(s.m_line);
                     todo_file->m_info.save_environment_options(s.m_line, s.m_env, s.m_options);
@@ -284,6 +286,7 @@ void server::interrupt_worker() {
 }
 
 static std::string * g_load = nullptr;
+static std::string * g_save = nullptr;
 static std::string * g_visit = nullptr;
 static std::string * g_sync = nullptr;
 static std::string * g_replace = nullptr;
@@ -352,6 +355,7 @@ void server::visit_file(std::string const & fname) {
         load_file(fname, error_if_nofile);
     } else {
         m_file = it->second;
+        m_cache.clear();
         process_from(0);
     }
 }
@@ -797,6 +801,20 @@ void server::wait(optional<unsigned> ms) {
     m_out << "-- ENDWAIT" << std::endl;
 }
 
+void server::save_olean(std::string const & fname) {
+    m_out << "-- BEGINSAVE" << std::endl;
+    check_file();
+    m_worker.wait(optional<unsigned>());
+    if (auto it = m_file->infom().get_final_env_opts()) {
+        std::ofstream out(fname, std::ofstream::binary);
+        environment const & env = it->first;
+        export_module(out, env);
+    } else {
+        m_out << "ERROR: nothing to be saved\n";
+    }
+    m_out << "-- ENDSAVE" << std::endl;
+}
+
 bool server::operator()(std::istream & in) {
     for (std::string line; std::getline(in, line);) {
         try {
@@ -804,6 +822,10 @@ bool server::operator()(std::istream & in) {
                 std::string fname = line.substr(g_load->size());
                 trim(fname);
                 load_file(fname);
+            } else if (is_command(*g_save, line)) {
+                std::string fname = line.substr(g_save->size());
+                trim(fname);
+                save_olean(fname);
             } else if (is_command(*g_visit, line)) {
                 std::string fname = line.substr(g_visit->size());
                 trim(fname);
@@ -877,6 +899,7 @@ bool server::operator()(std::istream & in) {
 void initialize_server() {
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     g_load = new std::string("LOAD");
+    g_save = new std::string("SAVE");
     g_visit = new std::string("VISIT");
     g_sync = new std::string("SYNC");
     g_replace = new std::string("REPLACE");
@@ -898,6 +921,7 @@ void initialize_server() {
 void finalize_server() {
     delete g_tmp_prefix;
     delete g_load;
+    delete g_save;
     delete g_visit;
     delete g_sync;
     delete g_replace;

src/frontends/lean/server.h

@@ -72,6 +72,7 @@ class server {
     worker                    m_worker;
 
     void load_file(std::string const & fname, bool error_if_nofile = true);
+    void save_olean(std::string const & fname);
     void visit_file(std::string const & fname);
     void check_file();
     void replace_line(unsigned line_num, std::string const & new_line);

src/library/module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include <sstream>
 #include <fstream>
 #include <algorithm>
+#include <sys/stat.h>
 #include "util/hash.h"
 #include "util/thread.h"
 #include "util/lean_path.h"
@@ -39,6 +40,10 @@ struct module_ext : public environment_extension {
     list<module_name> m_direct_imports;
     list<writer>      m_writers;
     name_set          m_module_defs;
+    // auxiliary information for detecting whether
+    // directly imported files have changed
+    list<time_t>      m_direct_imports_mod_time;
+    std::string       m_base;
 };
 
 struct module_ext_reg {
@@ -55,6 +60,35 @@ static environment update(environment const & env, module_ext const & ext) {
     return env.update(g_ext->m_ext_id, std::make_shared<module_ext>(ext));
 }
 
+list<module_name> get_direct_imports(environment const & env) {
+    return get_extension(env).m_direct_imports;
+}
+
+bool direct_imports_have_changed(environment const & env) {
+    module_ext const & ext   = get_extension(env);
+    std::string const & base = ext.m_base;
+    list<module_name> mods   = ext.m_direct_imports;
+    list<time_t>      mtimes = ext.m_direct_imports_mod_time;
+    lean_assert(length(mods) == length(mtimes));
+    while (mods && mtimes) {
+        module_name const & mname = head(mods);
+        std::string fname;
+        try {
+            fname = find_file(base, mname.get_k(), mname.get_name(), {".olean"});
+        } catch (exception &) {
+            return true; // direct import doesn't even exist anymore
+        }
+        struct stat st;
+        if (stat(fname.c_str(), &st) != 0)
+            return true; // failed to read stats
+        if (st.st_mtime != head(mtimes))
+            return true; // mod time has changed
+        mods   = tail(mods);
+        mtimes = tail(mtimes);
+    }
+    return false;
+}
+
 static char const * g_olean_end_file = "EndFile";
 static char const * g_olean_header   = "oleanfile";
 
@@ -235,7 +269,6 @@ struct import_modules_fn {
     }
 
     module_info_ptr load_module_file(std::string const & base, module_name const & mname) {
-        // TODO(Leo): support module_name
         std::string fname = find_file(base, mname.get_k(), mname.get_name(), {".olean"});
         auto it    = m_module_info.find(fname);
         if (it)
@@ -467,17 +500,25 @@ struct import_modules_fn {
         return env;
     }
 
-    void store_direct_imports(unsigned num_modules, module_name const * modules) {
+    void store_direct_imports(std::string const & base, unsigned num_modules, module_name const * modules) {
         m_senv.update([&](environment const & env) -> environment {
                 module_ext ext = get_extension(env);
-                for (unsigned i = 0; i < num_modules; i++)
+                ext.m_base     = base;
-                    ext.m_direct_imports = cons(modules[i], ext.m_direct_imports);
+                for (unsigned i = 0; i < num_modules; i++) {
+                    module_name const & mname = modules[i];
+                    ext.m_direct_imports = cons(mname, ext.m_direct_imports);
+                    std::string fname = find_file(base, mname.get_k(), mname.get_name(), {".olean"});
+                    struct stat st;
+                    if (stat(fname.c_str(), &st) != 0)
+                        throw exception(sstream() << "failed to access stats of file '" << fname << "'");
+                    ext.m_direct_imports_mod_time = cons(st.st_mtime, ext.m_direct_imports_mod_time);
+                }
                 return update(env, ext);
             });
     }
 
     environment operator()(std::string const & base, unsigned num_modules, module_name const * modules) {
-        store_direct_imports(num_modules, modules);
+        store_direct_imports(base, num_modules, modules);
         for (unsigned i = 0; i < num_modules; i++)
             load_module_file(base, modules[i]);
         process_asynch_tasks();

src/library/module.h

@@ -43,6 +43,13 @@ environment import_modules(environment const & env, std::string const & base, un
 environment import_module(environment const & env, std::string const & base, module_name const & module,
                           unsigned num_threads, bool keep_proofs, io_state const & ios);
 
+/** \brief Return the direct imports of the main module in the given environment. */
+list<module_name> get_direct_imports(environment const & env);
+
+/** \brief Return true iff the direct imports of the main module in the given environment have
+    been modified in the file system. */
+bool direct_imports_have_changed(environment const & env);
+
 /** \brief Store/Export module using \c env to the output stream \c out. */
 void export_module(std::ostream & out, environment const & env);
 

tests/lean/interactive/mod.input

@@ -0,0 +1,26 @@
+VISIT A.lean
+REPLACE 1
+definition id {A : Type} (a : A) := a
+SAVE A.olean
+VISIT B.lean
+REPLACE 1
+import A
+REPLACE 2
+definition my_id {A : Type} (a : A) := id a
+REPLACE 3
+definition my_id2 {A : Type} (a : A) := a
+WAIT
+EVAL
+check @my_id
+EVAL
+check @my_id2
+VISIT A.lean
+REPLACE 1
+definition id2 {A : Type} (a : A) := a
+SAVE A.olean
+VISIT B.lean
+WAIT
+EVAL
+check @my_id
+EVAL
+check @my_id2

tests/lean/interactive/mod.input.expected.out

@@ -0,0 +1,20 @@
+-- BEGINSAVE
+-- ENDSAVE
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINEVAL
+my_id : Π {A : Type}, A → A
+-- ENDEVAL
+-- BEGINEVAL
+my_id2 : Π {A : Type}, A → A
+-- ENDEVAL
+-- BEGINSAVE
+-- ENDSAVE
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINEVAL
+EVAL_command:1:7: error: unknown identifier 'my_id'
+-- ENDEVAL
+-- BEGINEVAL
+my_id2 : Π {A : Type}, A → A
+-- ENDEVAL