Reservoir

Izzimach/lean-glfw

C bindings and marshalling to use GLFW and OpenGL from the lean4 theorem prover

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

lean-glfw

Declarations and C thunks to allow access to GLFW and OpenGL from the lean4 theorem prover.

Emphasis is on using the bindless or Direct State Access method introduced in OpenGL 4.5. This means that binding objects and modifying "the current bound xxx" is discouraged and you should instead use functions that explicitly specify the buffer/VAO/program you are modifying.

building

To build and run this package you need access to both GLFW and it's dependencies. On windows this includes GDI32 which is provided by the Windows SDK.

Once you have these items installed you need to edit the lakefile to point to both GLFW and the Windows SDK.

At this point "lake build" should (hopefully) work.