feat(library/module, library/init/lean/environment): add primitives for reading/writing files as compacted regions

library/init/lean/environment.lean

@@ -283,9 +283,9 @@ structure ModuleData :=
 (entries    : Array (Name × Array EnvExtensionEntry))
 (serialized : ByteArray) -- Legacy support: serialized modification objects
 
-@[extern "lean_save_module_data"]
+@[extern 3 "lean_save_module_data"]
 constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := default _
-@[extern "lean_read_module_data"]
+@[extern 2 "lean_read_module_data"]
 constant readModuleData (fname : @& String) : IO ModuleData := default _
 
 def mkModuleData (env : Environment) : IO ModuleData :=

src/library/module.cpp

@@ -16,6 +16,8 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include "runtime/interrupt.h"
 #include "runtime/sstream.h"
 #include "runtime/hash.h"
+#include "runtime/io.h"
+#include "runtime/compact.h"
 #include "util/lean_path.h"
 #include "util/buffer.h"
 #include "util/name_map.h"
@@ -69,12 +71,63 @@ Missing features: non monotonic modifications in .olean files
 */
 
 namespace lean {
+static char const * g_olean_end_file = "EndFile";
+static char const * g_olean_header   = "oleanfile";
+
 extern "C" object * lean_save_module_data(object * fname, object * mdata, object * w) {
-    return w; // TODO
+    std::string olean_fn(string_cstr(fname));
+    object_ref mdata_ref(mdata);
+    try {
+        exclusive_file_lock output_lock(olean_fn);
+        std::ofstream out(olean_fn, std::ios_base::binary);
+        if (out.fail()) {
+            return set_io_error(w, (sstream() << "failed to create file '" << olean_fn << "'").str());
+        }
+        object_compactor compactor;
+        compactor(mdata_ref.raw());
+        out.write(g_olean_header, strlen(g_olean_header));
+        out.write(static_cast<char const *>(compactor.data()), compactor.size());
+        out.close();
+        return set_io_result(w, box(0));
+    } catch (exception & ex) {
+        return set_io_error(w, (sstream() << "failed to write '" << olean_fn << "': " << ex.what()).str());
+    }
 }
 
 extern "C" object * lean_read_module_data(object * fname, object * w) {
-    return w; // TODO
+    std::string olean_fn(string_cstr(fname));
+    try {
+        shared_file_lock olean_lock(olean_fn);
+        std::ifstream in(olean_fn, std::ios_base::binary);
+        if (in.fail()) {
+            return set_io_error(w, (sstream() << "failed to open file '" << olean_fn << "'").str());
+        }
+        /* Get file size */
+        in.seekg(0, in.end);
+        size_t size = in.tellg();
+        in.seekg(0);
+        size_t header_size = strlen(g_olean_header);
+        if (size < header_size) {
+            return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
+        }
+        char header[header_size];
+        in.read(header, header_size);
+        if (strncmp(header, g_olean_header, header_size) != 0) {
+            return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
+        }
+        char * buffer = new char[size - header_size];
+        in.read(buffer, size - header_size);
+        if (!in) {
+            return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "'").str());
+        }
+        in.close();
+        /* We don't free compacted_region objects */
+        compacted_region * region = new compacted_region(size - header_size, buffer);
+        object * mod = region->read();
+        return set_io_result(w, mod);
+    } catch (exception & ex) {
+        return set_io_error(w, (sstream() << "failed to read '" << olean_fn << "': " << ex.what()).str());
+    }
 }
 
 static void modification_finalizer(void * ext) {
@@ -119,9 +172,6 @@ static environment update(environment const & env, module_ext const & ext) {
     return env.update(g_ext->m_ext_id, new module_ext(ext));
 }
 
-static char const * g_olean_end_file = "EndFile";
-static char const * g_olean_header   = "oleanfile";
-
 static unsigned olean_hash(std::string const & data) {
     return hash(data.size(), [&] (unsigned i) { return static_cast<unsigned char>(data[i]); });
 }

src/runtime/io.cpp

@@ -16,7 +16,7 @@ void io_result_show_error(b_obj_arg r) {
     std::cerr << "uncaught exception: " << string_cstr(io_result_get_error(r)) << std::endl;
 }
 
-static obj_res set_io_result(obj_arg r, obj_arg a) {
+obj_res set_io_result(obj_arg r, obj_arg a) {
     if (is_exclusive(r)) {
         cnstr_set(r, 0, a);
         return r;
@@ -29,7 +29,7 @@ static obj_res set_io_result(obj_arg r, obj_arg a) {
     }
 }
 
-static obj_res set_io_error(obj_arg r, obj_arg e) {
+obj_res set_io_error(obj_arg r, obj_arg e) {
     if (is_exclusive(r)) {
         cnstr_set_tag(r, 1);
         cnstr_set(r, 0, e);
@@ -43,6 +43,19 @@ static obj_res set_io_error(obj_arg r, obj_arg e) {
     }
 }
 
+object * mk_io_user_error(object * str) {
+    // TODO(Leo): fix after we expand IO.Error
+    return str;
+}
+
+obj_res set_io_error(obj_arg r, char const * msg) {
+    return set_io_error(r, mk_io_user_error(mk_string(msg)));
+}
+
+obj_res set_io_error(obj_arg r, std::string const & msg) {
+    return set_io_error(r, mk_io_user_error(mk_string(msg)));
+}
+
 static obj_res option_of_io_result(obj_arg r) {
     if (io_result_is_ok(r)) {
         object * o = alloc_cnstr(1, 1, 0);

src/runtime/io.h

@@ -5,7 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "runtime/object.h"
 namespace lean {
+obj_res set_io_result(obj_arg r, obj_arg a);
+obj_res set_io_error(obj_arg r, obj_arg e);
+obj_res set_io_error(obj_arg r, char const * msg);
+obj_res set_io_error(obj_arg r, std::string const & msg);
 void initialize_io();
 void finalize_io();
 }

src/stage0/init/lean/environment.cpp

@@ -83,6 +83,7 @@ obj* l_RBNode_find___main___at_Lean_Environment_find___spec__2___boxed(obj*, obj
 obj* l_Lean_registerEnvExtensionUnsafe___rarg(obj*, obj*);
 obj* l_AssocList_contains___main___at_Lean_Environment_add___spec__5___boxed(obj*, obj*);
 extern "C" usize lean_name_hash_usize(obj*);
+obj* l_Lean_readModuleData___boxed(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_getState___rarg(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_getEntries___boxed(obj*, obj*);
 obj* l_Lean_EnvExtension_getStateUnsafe___rarg___boxed(obj*, obj*);
@@ -98,6 +99,7 @@ obj* l_Lean_PersistentEnvExtension_getEntries(obj*, obj*);
 obj* l_Lean_PersistentEnvExtensionState_inhabited;
 obj* l___private_init_lean_environment_6__envExtensionsRef;
 obj* l_Lean_EnvExtension_getState___boxed(obj*);
+extern "C" obj* lean_save_module_data(obj*, obj*, obj*);
 obj* l_Lean_EnvExtension_getState___rarg(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_forceStateAux(obj*, obj*);
 namespace lean {
@@ -116,6 +118,7 @@ namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
 }
 obj* l_Lean_EnvExtension_setStateUnsafe___rarg(obj*, obj*, obj*);
+obj* l_Lean_saveModuleData___boxed(obj*, obj*, obj*);
 uint8 l_RBNode_isRed___main___rarg(obj*);
 namespace lean {
 obj* set_extension_core(obj*, obj*, obj*);
@@ -145,6 +148,7 @@ extern obj* l_NonScalar_Inhabited;
 obj* l_List_foldl___main___rarg(obj*, obj*, obj*);
 obj* l_Lean_Environment_contains___boxed(obj*, obj*);
 obj* l___private_init_lean_environment_3__isQuotInit___boxed(obj*);
+extern "C" obj* lean_read_module_data(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_addEntry___boxed(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_getState___boxed(obj*, obj*);
 obj* l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__2;
@@ -4318,6 +4322,24 @@ x_1 = lean_serialize_modifications(x_0);
 return x_1;
 }
 }
+obj* l_Lean_saveModuleData___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean_save_module_data(x_0, x_1, x_2);
+lean::dec(x_0);
+return x_3;
+}
+}
+obj* l_Lean_readModuleData___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean_read_module_data(x_0, x_1);
+lean::dec(x_0);
+return x_2;
+}
+}
 obj* l_Nat_foldAux___main___at_Lean_mkModuleData___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {

src/util/string_ref.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include "runtime/sstream.h"
 #include "util/object_ref.h"
 #include "util/list_ref.h"
 namespace lean {
@@ -14,6 +15,7 @@ class string_ref : public object_ref {
 public:
     explicit string_ref(char const * s):object_ref(mk_string(s)) {}
     explicit string_ref(std::string const & s):object_ref(mk_string(s)) {}
+    explicit string_ref(sstream const & strm):string_ref(strm.str()) {}
     string_ref(string_ref const & other):object_ref(other) {}
     string_ref(string_ref && other):object_ref(other) {}
     explicit string_ref(obj_arg o):object_ref(o) {}

tests/playground/moddata.lean

@@ -0,0 +1,21 @@
+import init.lean.environment
+open Lean
+
+def saveTestFile (fn : String) : IO Unit :=
+saveModuleData fn {
+  imports    := [`foo, `bla].toArray,
+  constants  := Array.empty,
+  entries    := Array.empty,
+  serialized := [1, 2, 3, 4].toByteArray
+}
+
+def openTestFile (fn : String) : IO Unit :=
+do m ← readModuleData fn,
+   IO.println m.imports,
+   IO.println m.serialized,
+   pure ()
+
+def main (xs : List String) : IO Unit :=
+let fn := xs.head in
+saveTestFile fn *>
+openTestFile fn