max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/environment): add placeholders for writing/reading .olean files

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-13 15:48:23 -07:00
parent 31d140adab
commit 40f9704540
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/environment.lean
View file

@ -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,

8
src/library/module.cpp
View file

@ -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);
}