Siddharth

Done once again, I've made changes as requested by @Kha , @gebner .

@Kha , if we could merge this, I can make progress on https://github.com/leanprover/lean4/pull/1837, since there's code there I'd like to split across PRs, but the diffs would be too big...

[Z3's bitvector theory](https://microsoft.github.io/z3guide/docs/theories/Bitvectors/) seems to provide separate `ashr` and `lshr` instructions, while the [`smtlib2` documentation](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml) seems to only have `lshr`. Is this a Z3 specific extension? I would really like...

@locriacyber Thanks for the PR! Ideally, all uses of `size_t` / platform dependent width should be localized to [`size_tType`](https://github.com/leanprover/lean4/blob/c45f1b5f0b04189af977d0776c817a02ed4c0bd7/src/Lean/Compiler/IR/EmitLLVM.lean#L28-L29). We should change its definition to build an `i`. I also...

Heya @iacore , thanks again for the PR! I'm now in a position to review and merge this PR, if you have the bandwidth to rebase this on top of...

were (@hargoniX and I) are testing the code that's generated by this PR before we greenlight it. In doing so, we've discovered a curious bug: ``` $ ../../build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean...

We do indeed miscompile: ``` $ ../../build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean --bc=closure_bug7.bc ... lean: /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Instructions.cpp:528: void llvm::CallInst::init(llvm::FunctionType*, llvm::Value*, llvm::ArrayRef, llvm::ArrayRef, const llvm::Twine&): Assertion `(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling...

I'm now attempting to fix the trail of issues this has unearthed here: https://github.com/bollu/lean4/tree/llvm-size_t @iacore , I've given you push access to the repo `bollu/lean4`. Shall we continue developing this...

We appear to have fixed the prior issue with code generating `lean_box`, and are now attempting to fix the argument list of `lean_ctor_set_arg`. Here's the backtrace: https://github.com/bollu/lean4/commit/1f617201f011d3c724d4dadd24bc20c1f667890f

@iacore one needs to build LLVM with a debug build. When compiling LLVM, we run `cmake ../ -DLLVM_ENABLE_ASSERTIONS=ON -DCMAKE_BUILD_TYPE=Debug -DLLVM_ENABLE_EXPENSIVE_CHECKS=ON`. Then, we use this version of the LLVM toolchain to...