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.
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.