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

chore: remove obsolete workaround

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-23 17:46:46 +01:00
parent 1c4460a206
commit f4ef29b800
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Server/FileWorker.lean
View file

@ -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
end Lean.Server.FileWorker