fix: enable initialisers in Extract[Module] (#81)

Prior to this change, `subverso-extract` and `subverso-extract-mod`
would fail on any module that imports a non-core module with `initialize`
declarations.

Co-authored-by: Jannis Limperg <[email protected]>

Author: JLimperg

Extract.lean

@@ -9,11 +9,12 @@ import SubVerso.Examples.Env
 open Lean
 open SubVerso.Examples
 
-def main : (args : List String) → IO UInt32
+unsafe def main : (args : List String) → IO UInt32
   | [mod, outFile] => do
     try
       initSearchPath (← findSysroot)
       let modName := mod.toName
+      enableInitializersExecution
       let env ← SubVerso.Compat.importModules #[{module := modName, runtimeOnly := false}] {}
       let modExamples := highlighted.getState env
       let useful := relevant modName modExamples

ExtractModule.lean

@@ -12,8 +12,7 @@ open Lean.Elab.Command (liftTermElabM)
 open SubVerso Examples
 open SubVerso.Highlighting (Highlighted highlight)
 
-
-def main : (args : List String) → IO UInt32
+unsafe def main : (args : List String) → IO UInt32
   | [mod, outFile] => do
     try
       initSearchPath (← findSysroot)
@@ -29,6 +28,7 @@ def main : (args : List String) → IO UInt32
       let ictx := Parser.mkInputContext (← IO.FS.readFile fname) fname.toString
       let (headerStx, parserState, msgs) ← Parser.parseHeader ictx
       let imports := headerToImports headerStx
+      enableInitializersExecution
       let env ← importModules imports {}
       let pctx : Context := {inputCtx := ictx}
 
@@ -55,6 +55,3 @@ def main : (args : List String) → IO UInt32
   | other => do
     IO.eprintln s!"Didn't understand args: {other}"
     pure 1
-where
-  relevant (mod : Name) (examples : NameMap (NameMap Json)) : List (String × Json) :=
-    examples.find? mod |>.getD {} |>.toList |>.map fun p => {p with fst := p.fst.toString (escape := false)}