diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean
index 3343945348..f2d72f464a 100644
--- a/library/init/lean/environment.lean
+++ b/library/init/lean/environment.lean
@@ -283,6 +283,11 @@ structure ModuleData :=
 (entries    : Array (Name × Array EnvExtensionEntry))
 (serialized : ByteArray) -- Legacy support: serialized modification objects
 
+@[extern "lean_save_module_data"]
+constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := default _
+@[extern "lean_read_module_data"]
+constant readModuleData (fname : @& String) : IO ModuleData := default _
+
 def mkModuleData (env : Environment) : IO ModuleData :=
 do
 pExts ← persistentEnvExtensionsRef.get,
diff --git a/src/library/module.cpp b/src/library/module.cpp
index a0fa59a353..3a2ec63f60 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -69,6 +69,14 @@ Missing features: non monotonic modifications in .olean files
 */
 
 namespace lean {
+extern "C" object * lean_save_module_data(object * fname, object * mdata, object * w) {
+    return w; // TODO
+}
+
+extern "C" object * lean_read_module_data(object * fname, object * w) {
+    return w; // TODO
+}
+
 static void modification_finalizer(void * ext) {
     delete static_cast<modification*>(ext);
 }