GUI in Lean

Stream: lean4

[Martin Dvořák]

Is it possible to create apps with GUI in Lean?
Do we have something like WinForms but compatible with Lean?

[Anand Rao Tadipatri]

Is the application meant to be standalone, or something that runs in the Lean infoview?

[Max Nowak 🐉]

Me and Arthur were trying to create wgpu bindings for Lean, and we managed to a triangle :red_triangle_up: . But then other life obligations hit. This is obviously very very far away from a GUI.

...alternatively, you could (ab)use userwidgets/proofwidgets, but then you're confined to the infoview.

[Daniil Kisel]

Raylib bindings include raygui, it is a simple immediate mode gui library without state management or automatic layout (I've also made yoga bindings, but to properly utilise them you'll need to implement tree/state management yourself).

It is also possible to make your app a web server with gui presented in a browser. Simple to implement with cgi using only IO.print (apart from external setup). There were some web server related projects.