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

fix: metadata codegen for LLVM

Browse source
This commit is contained in:
Siddharth Bhat 2023-01-09 11:33:28 +00:00 • committed by Sebastian Ullrich
parent 67a5846742
commit ae4f2de951
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Compiler/IR/EmitLLVM.lean
View file

@ -1079,10 +1079,7 @@ partial def emitBlock (builder : LLVM.Builder llvmctx) (b : FnBody) : M llvmctx
| FnBody.set x i y b => emitSet builder x i y; emitBlock builder b
| FnBody.uset x i y b => emitUSet builder x i y; emitBlock builder b
| FnBody.sset x i o y t b => emitSSet builder x i o y t; emitBlock builder b
| FnBody.mdata _ _b =>
-- TODO(bollu) : implement `mdata`.
-- NOTE(bollu) : It is disturbing that we pass the Lean CI without this.
throw "Unimplemented metadata."
| FnBody.mdata _ b => emitBlock builder b
| FnBody.ret x => do
let (_xty, xv) ← emitArgVal builder x "ret_val"
let _ ← LLVM.buildRet builder xv