From ae4f2de9513354c79f933ade4b35439bd92ac837 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 9 Jan 2023 11:33:28 +0000 Subject: [PATCH] fix: metadata codegen for LLVM --- src/Lean/Compiler/IR/EmitLLVM.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 365e0b7012..79f84734d0 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/src/Lean/Compiler/IR/EmitLLVM.lean @@ -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