Siddharth

Create a simpler version of the attribute tutorial by covering whatever Leo did at the post ICERM hackathon.

It's confusing as a newbie to arrive at this repo and have no context whatsoever. Instead, we link to the nix wiki instead to point people to an explanation.

Bump up to LLVM 15

2

Let us refactor the patch that adds LLVM support to Lean4 into another component: We first bump up LLVM to LLVM 15, and then add the bindings. We see that...

feat: add LLVM C API bindings

4

This makes the following changes: 1. It adds a `src/Lean/Compiler/IR/LLVMBindings.lean` with the C API bindings required for the LLVM backend 2. It adds a stub `src/Lean/Compiler/IR/EmitLLVM.cpp`, to import `LLVMBindings` and...

feat: add more raw bitvector functions

1

This adds `_unsafe` versions for modulo, shift left and shift right.

feat: characterize BitVec.toInt in terms of BitVec.toNat

4

This characterizes `toInt` in terms of `toNat`. This PR is stacked on https://github.com/leanprover/lean4/pull/3480 to write the theorems in a style that includes the width zero case.

feat: add BitVec.ult/ule_ofNat

5

This supersedes https://github.com/leanprover/std4/pull/664, and adds lemmas that mirror `ofNat_{add,sub}_ofNat` for ult, ule.

Replacement Bookmark Package

1

Hey! I too have written a [bookmark system for sublime text](https://github.com/bollu/sublimeBookmark) I found that your package has not been maintaned for > 2 years, so I decided to build my...

Add ZLib dependency into profiler

3

This fixes missing dependencies when compiling tracy-profiler with LEGACY=ON: ``` [100%] Linking CXX executable tracy-profiler lto-wrapper: warning: using serial compilation of 6 LTRANS jobs /usr/bin/ld: /usr/local/lib/libfreetype.a(ftgzip.c.o): in function `ft_gzip_file_fill_output': /homes/sb2743/2024-borrowing/tracy/build/profiler/_deps/freetype-src/src/gzip/ftgzip.c:439:...