From 58449131020dcd29be1c8c4b9de62daa465da82b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 May 2019 17:24:45 -0700 Subject: [PATCH] feat(library/module, library/init/lean/environment): add primitives for reading/writing files as compacted regions --- library/init/lean/environment.lean | 4 +- src/library/module.cpp | 60 +++++++++++++++++++++++++--- src/runtime/io.cpp | 17 +++++++- src/runtime/io.h | 5 +++ src/stage0/init/lean/environment.cpp | 22 ++++++++++ src/util/string_ref.h | 2 + tests/playground/moddata.lean | 21 ++++++++++ 7 files changed, 122 insertions(+), 9 deletions(-) create mode 100644 tests/playground/moddata.lean diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index f2d72f464a..bea18db21b 100644 --- a/library/init/lean/environment.lean +++ b/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 := diff --git a/src/library/module.cpp b/src/library/module.cpp index 3a2ec63f60..72bfad1748 100644 --- a/src/library/module.cpp +++ b/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(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(data[i]); }); } diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index eb4b162b43..91274b0b3f 100644 --- a/src/runtime/io.cpp +++ b/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); diff --git a/src/runtime/io.h b/src/runtime/io.h index a6eedf3502..6aea01a0a5 100644 --- a/src/runtime/io.h +++ b/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(); } diff --git a/src/stage0/init/lean/environment.cpp b/src/stage0/init/lean/environment.cpp index 02200c42bf..18032180d4 100644 --- a/src/stage0/init/lean/environment.cpp +++ b/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: { diff --git a/src/util/string_ref.h b/src/util/string_ref.h index 990ea019a3..98cebec546 100644 --- a/src/util/string_ref.h +++ b/src/util/string_ref.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#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) {} diff --git a/tests/playground/moddata.lean b/tests/playground/moddata.lean new file mode 100644 index 0000000000..0badfdfd8a --- /dev/null +++ b/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