From bad62333897ae410f8fac93f1e8d6f992bdd06d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 08:10:51 -0700 Subject: [PATCH] chore: remove legacy support for modification objects --- src/Lean/Environment.lean | 38 +---- src/library/CMakeLists.txt | 3 +- src/library/compiler/borrowed_annotation.cpp | 1 - src/library/compiler/closed_term_cache.cpp | 1 - src/library/compiler/eager_lambda_lifting.cpp | 1 - src/library/compiler/specialize.cpp | 1 - src/library/init_module.cpp | 3 - src/library/module.cpp | 132 ------------------ src/library/module.h | 42 ------ src/library/protected.cpp | 1 - src/shell/lean_js.cpp | 1 - 11 files changed, 3 insertions(+), 221 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 1753035068..78e7f568fa 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -444,45 +444,15 @@ def isTagged (ext : TagDeclarationExtension) (env : Environment) (n : Name) : Bo end TagDeclarationExtension -/- Legacy support for Modification objects -/ - -/- Opaque modification object. It is essentially a C `void *`. - In Lean 3, a .olean file is essentially a collection of modification objects. - This type represents the modification objects implemented in C++. - We will eventually delete this type as soon as we port the remaining Lean 3 - legacy code. - - TODO: delete after we remove legacy code -/ -def Modification := NonScalar - -instance : Inhabited Modification := inferInstanceAs (Inhabited NonScalar) - -builtin_initialize modListExtension : EnvExtension (List Modification) ← registerEnvExtension (pure []) - - -/- The C++ code uses this function to store the given modification object into the environment. -/ -@[export lean_environment_add_modification] -def addModification (env : Environment) (mod : Modification) : Environment := - modListExtension.modifyState env $ fun mods => mod :: mods - -/- mkModuleData invokes this function to convert a list of modification objects into - a serialized byte array. -/ -@[extern 2 "lean_serialize_modifications"] -constant serializeModifications : List Modification → IO ByteArray - -@[extern 3 "lean_perform_serialized_modifications"] -constant performModifications : Environment → ByteArray → IO Environment - /- Content of a .olean file. We use `compact.cpp` to generate the image of this object in disk. -/ structure ModuleData := (imports : Array Import) (constants : Array ConstantInfo) (entries : Array (Name × Array EnvExtensionEntry)) - (serialized : ByteArray) -- Legacy support: serialized modification objects instance : Inhabited ModuleData := - ⟨{imports := arbitrary _, constants := arbitrary _, entries := arbitrary _, serialized := arbitrary _}⟩ + ⟨{imports := arbitrary _, constants := arbitrary _, entries := arbitrary _}⟩ @[extern 3 "lean_save_module_data"] constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit @@ -520,12 +490,10 @@ def mkModuleData (env : Environment) : IO ModuleData := do let extName := (pExts.get! i).name result.push (extName, exportEntriesFn state)) #[] - let bytes ← serializeModifications (modListExtension.getState env) pure { imports := env.header.imports, constants := env.constants.foldStage2 (fun cs _ c => cs.push c) #[], - entries := entries, - serialized := bytes + entries := entries } @[export lean_write_module] @@ -599,8 +567,6 @@ def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 } let env ← setImportedEntries env mods let env ← finalizePersistentExtensions env opts - for mod in mods do - env ← performModifications env mod.serialized pure env /-- diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 457878da25..a7fcf7a3f5 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,7 +1,6 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp io_state_stream.cpp bin_app.cpp constants.cpp max_sharing.cpp - module.cpp placeholder.cpp - sorry.cpp replace_visitor.cpp num.cpp + module.cpp placeholder.cpp sorry.cpp replace_visitor.cpp num.cpp class.cpp util.cpp print.cpp annotation.cpp protected.cpp reducible.cpp init_module.cpp exception.cpp pp_options.cpp projection.cpp diff --git a/src/library/compiler/borrowed_annotation.cpp b/src/library/compiler/borrowed_annotation.cpp index a5cc0d1ae3..17ed3f7761 100644 --- a/src/library/compiler/borrowed_annotation.cpp +++ b/src/library/compiler/borrowed_annotation.cpp @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/instantiate.h" -#include "library/module.h" #include "library/trace.h" #include "library/annotation.h" #include "library/compiler/util.h" diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp index a117ea17cd..2dbdfa40dd 100644 --- a/src/library/compiler/closed_term_cache.cpp +++ b/src/library/compiler/closed_term_cache.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/module.h" #include "library/util.h" namespace lean { diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp index ec203e6271..b950d693bb 100644 --- a/src/library/compiler/eager_lambda_lifting.cpp +++ b/src/library/compiler/eager_lambda_lifting.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/type_checker.h" #include "library/trace.h" -#include "library/module.h" #include "library/class.h" #include "library/compiler/util.h" #include "library/compiler/csimp.h" diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 27ce7477f1..ed4ac6cd91 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "library/class.h" #include "library/trace.h" -#include "library/module.h" #include "library/compiler/util.h" #include "library/compiler/csimp.h" diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 2ec53fb879..ecf7e219d7 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/num.h" #include "library/annotation.h" -#include "library/module.h" #include "library/protected.h" #include "library/io_state.h" #include "library/idx_metavar.h" @@ -38,11 +37,9 @@ void initialize_library_core_module() { initialize_constants(); initialize_profiling(); initialize_trace(); - initialize_module(); } void finalize_library_core_module() { - finalize_module(); finalize_trace(); finalize_profiling(); finalize_constants(); diff --git a/src/library/module.cpp b/src/library/module.cpp index 2d679d97be..310c47e2e0 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -103,102 +103,6 @@ extern "C" object * lean_read_module_data(object * fname, object *) { } } -// ======================================= -// Legacy support for Lean3 modification objects - -static void modification_finalizer(void * ext) { - delete static_cast(ext); -} - -static void modification_foreach(void * /* mod */, b_obj_arg /* fn */) { -} - -static external_object_class * g_modification_class = nullptr; - -static modification & to_modification(b_obj_arg o) { - lean_assert(external_class(o) == g_modification_class); - return *static_cast(external_data(o)); -} - -static obj_res to_object(modification * ext) { - return alloc_external(g_modification_class, ext); -} - -typedef std::unordered_map object_readers; -static object_readers * g_object_readers = nullptr; -static object_readers & get_object_readers() { return *g_object_readers; } - -void register_module_object_reader(std::string const & k, module_modification_reader && r) { - object_readers & readers = get_object_readers(); - lean_assert(readers.find(k) == readers.end()); - readers[k] = r; -} - -static char const * g_olean_end_file = "EndFile"; - -extern "C" object * lean_serialize_modifications(object * mod_list, object *) { - object_ref mod_list_ref(mod_list); - try { - std::ostringstream out(std::ios_base::binary); - serializer s(out); - buffer mod_buffer; - while (!is_scalar(mod_list)) { - mod_buffer.push_back(cnstr_get(mod_list, 0)); - mod_list = cnstr_get(mod_list, 1); - } - size_t i = mod_buffer.size(); - while (i > 0) { - --i; - modification & mod = to_modification(mod_buffer[i]); - s << std::string(mod.get_key()); - mod.serialize(s); - } - s << g_olean_end_file; - std::string bytes = out.str(); - - object * r = alloc_sarray(1, bytes.size(), bytes.size()); - memcpy(sarray_cptr(r), bytes.data(), bytes.size()); - - return io_result_mk_ok(r); - } catch (exception & ex) { - return io_result_mk_error(ex.what()); - } -} - -extern "C" object * lean_perform_serialized_modifications(object * env0, object * bytes, object *) { - environment env(env0); - std::string code((char*)sarray_cptr(bytes), sarray_size(bytes)); - dec_ref(bytes); - try { - std::istringstream in(code, std::ios_base::binary); - deserializer d(in); - object_readers & readers = get_object_readers(); - while (true) { - std::string k; - unsigned offset = in.tellg(); - d >> k; - if (k == g_olean_end_file) { - break; - } - auto it = readers.find(k); - if (it == readers.end()) - throw exception(sstream() << "olean file has been corrupted at offset " << offset - << ", unknown object: " << k); - modification * mod = it->second(d); - mod->perform(env); - delete mod; - } - if (!in.good()) { - throw exception(sstream() << "olean file has been corrupted"); - } - return io_result_mk_ok(env.steal()); - } catch (exception & ex) { - return io_result_mk_error(ex.what()); - } -} - -// ======================================= - /* @[export lean.write_module_core] def writeModule (env : Environment) (fname : String) : IO Unit := */ @@ -207,40 +111,4 @@ extern "C" object * lean_write_module(object * env, object * fname, object *); void write_module(environment const & env, std::string const & olean_fn) { consume_io_result(lean_write_module(env.to_obj_arg(), mk_string(olean_fn), io_mk_world())); } - -extern "C" object * lean_import_modules(object * imports, object * opts, uint32 trust_level, object * w); - -environment import_modules(unsigned trust_lvl, options const & opts, object_ref const & imports) { - return get_io_result(lean_import_modules(imports.to_obj_arg(), opts.to_obj_arg(), trust_lvl, io_mk_world())); -} - -extern "C" object * lean_environment_add_modification(object * env, object * mod); - -namespace module { -environment add(environment const & env, modification* modf) { - return environment(lean_environment_add_modification(env.to_obj_arg(), to_object(modf))); -} - -environment add_and_perform(environment const & env, modification * modf) { - auto new_env = env; - modf->perform(new_env); - return add(new_env, modf); -} - -environment add(environment const & env, declaration const & d, bool check) { - return env.add(d, check); -} -} // end of namespace module - -void initialize_module() { - // file header size should preserve alignment - // can't be a static_assert because strlen isn't constexpr... - lean_always_assert(strlen(g_olean_header) % sizeof(object *) == 0); - g_modification_class = register_external_object_class(modification_finalizer, modification_foreach); - g_object_readers = new object_readers(); -} - -void finalize_module() { - delete g_object_readers; -} } diff --git a/src/library/module.h b/src/library/module.h index e293802f5f..674951de4d 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -15,48 +15,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include "kernel/environment.h" namespace lean { -using module_name = name; -/** \brief Return an environment where all modules in \c modules are imported. - Modules included directly or indirectly by them are also imported. - - This procedure looks for imported files in the search path set using `set_search_path`. */ -environment import_modules(unsigned trust_lvl, options const &, object_ref const & imports); - /** \brief Store module using \c env. */ void write_module(environment const & env, std::string const & olean_fn); - -struct modification { -public: - virtual ~modification() {} - virtual const char * get_key() const = 0; - virtual void perform(environment &) const = 0; - virtual void serialize(serializer &) const = 0; -}; - -#define LEAN_MODIFICATION(k) \ - static void init() { \ - register_module_object_reader(k, module_modification_reader(deserialize)); \ - } \ - static void finalize() {} \ - const char * get_key() const override { return k; } - -using module_modification_reader = std::function; - -/** \brief Register a module object reader. The key \c k is used to identify the class of objects - that can be read by the given reader. -*/ -void register_module_object_reader(std::string const & k, module_modification_reader && r); - -namespace module { -/** \brief Add a function that should be invoked when the environment is exported. - The key \c k identifies which module_object_reader should be used to deserialize the object - when the module is imported. - - \see module_object_reader -*/ -environment add(environment const & env, modification * modif); -environment add_and_perform(environment const & env, modification * modif); -} -void initialize_module(); -void finalize_module(); } diff --git a/src/library/protected.cpp b/src/library/protected.cpp index 863a95575a..d2e2e85420 100644 --- a/src/library/protected.cpp +++ b/src/library/protected.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include "util/name_set.h" #include "library/protected.h" -#include "library/module.h" namespace lean { extern "C" object * lean_add_protected(object * env, object * n); diff --git a/src/shell/lean_js.cpp b/src/shell/lean_js.cpp index 55a4fc7224..4c2a75d0cb 100644 --- a/src/shell/lean_js.cpp +++ b/src/shell/lean_js.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include #include "library/module_mgr.h" #include "library/st_task_queue.h" -#include "library/module.h" #include "library/type_context.h" #include "frontends/lean/pp.h" #include "frontends/lean/parser.h"