diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index a4931bd969..b2da377837 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -127,9 +127,7 @@ section ServerM def compileDocument (m : DocumentMeta) : ServerM Unit := do let headerSnap@⟨_, _, _, SnapshotData.headerData env msgLog opts⟩ ← Snapshots.compileHeader m.text.source | throwServerError "Internal server error: invalid header snapshot" - -- TODO(WN): Remove the hardcoded option once the server is linked against stage0 - let opts' := opts.setBool `interpreter.prefer_native false - let headerSnap' := { headerSnap with data := SnapshotData.headerData env msgLog opts' } + let headerSnap' := { headerSnap with data := SnapshotData.headerData env msgLog opts } let cmdSnaps ← unfoldCmdSnaps m headerSnap (←read).docRef.set ⟨m, headerSnap, cmdSnaps⟩ @@ -310,4 +308,4 @@ def workerMain : IO UInt32 := do e.putStrLn (toString err) return 1 -end Lean.Server.FileWorker \ No newline at end of file +end Lean.Server.FileWorker