Trying to make wgpu bindings for Lean.
Currently, you need to download the wgpu_native release from github releases and put it in a folder in the repo root. Might have to adjust wgpu_native_dir in the lakefile yourself currently.
Helpful resources for dealing with FFI (only relevant if you want to dev these bindings):
- Lake readme: https://github.com/leanprover/lean4/tree/master/src/lake
- Non-alloy FFI, and Lean ABI: https://lean-lang.org/lean4/doc/dev/ffi.html
- Lakefile FFI example: https://github.com/leanprover/lean4/blob/master/src/lake/examples/ffi/lib/lakefile.lean
- Zulip thread about this repo, how to set up Lake with Alloy for wgpu: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lake.2BAlloy.3A.20Using.20external.20C.20library/near/442743388
- "S" Example
- WebGPU Guide. For C++, but explains concepts well, and... just adapt it to C: https://eliemichel.github.io/LearnWebGPU/getting-started/opening-a-window.html
Currently, you need to download the wgpu_native release from github releases and put it in a folder in the repo root. Might have to adjust wgpu_native_dir in the lakefile yourself currently.
You need to install glfw, ideally via your system package manager.
- macOS:
brew install glfw, thenbrew --prefix glfwshould print something like/opt/homebrew/opt/glfw. - Linux: (Add info here)
- Windows: (Add info here)