Make the webcam demo run on macOS

Lean runs main on a helper thread, which Cocoa rejects for video init;
export LEAN_MAIN_USE_THREAD=0 from the justfile on macOS. Wait for the
camera permission event before reading the camera format, since SDL
grants access asynchronously.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

README.md

@@ -29,9 +29,16 @@ lean_exe «lean-sdl-test» where
   root := `Main
   -- this is necessary because on Linux, binaries don't automatically get picked up by the executable unless you set the rpath
   -- also, moreLinkArgs doesn't get inherited by the parent project
-  moreLinkArgs := if !System.Platform.isWindows then #["-Wl,--allow-shlib-undefined", "-Wl,-rpath=$ORIGIN"] else #[]
+  moreLinkArgs :=
+    if System.Platform.isWindows then #[]
+    else if System.Platform.isOSX then #["-Wl,-undefined,dynamic_lookup", "-Wl,-rpath,@executable_path"]
+    else #["-Wl,--allow-shlib-undefined", "-Wl,-rpath=$ORIGIN"]
 ```
 
+On macOS, run the executable with `LEAN_MAIN_USE_THREAD=0`. Lean's runtime otherwise runs `main` on a
+helper thread, and Cocoa refuses to create a video device off the main thread (`SDL_Init` fails with
+"No available video device"). The `justfile` recipes set this for you.
+
 
 ## Acknowledgements
 MASSIVE thanks to Oliver Dressler (@oOo0oOo) and Mac Malone (@tydeu) for all the help they gave!

SDL.lean

@@ -21,6 +21,8 @@ def SDL_INIT_CAMERA: UInt32 := 0x00010000
 def SDL_WINDOW_SHOWN : UInt32 := 0x00000004
 def SDL_RENDERER_ACCELERATED : UInt32 := 0x00000002
 def SDL_QUIT : UInt32 := 0x100
+def SDL_EVENT_CAMERA_DEVICE_APPROVED : UInt32 := 0x1402
+def SDL_EVENT_CAMERA_DEVICE_DENIED : UInt32 := 0x1403
 
 def SDL_SCANCODE_W : UInt32 := 26
 def SDL_SCANCODE_A : UInt32 := 4

WebcamApp.lean

@@ -5,6 +5,18 @@ def SCREEN_HEIGHT : Int32 := 720
 
 def isEscapeKeyDown : IO Bool := SDL.getKeyState SDL.SDL_SCANCODE_ESCAPE
 
+-- SDL reports camera permission asynchronously (macOS shows a system prompt); the format and
+-- frames are unavailable until the approved event arrives.
+partial def waitForCameraPermission : IO Bool := do
+  let eventType ← SDL.pollEvent
+  if eventType == SDL.SDL_EVENT_CAMERA_DEVICE_APPROVED then
+    return true
+  if eventType == SDL.SDL_EVENT_CAMERA_DEVICE_DENIED || eventType == SDL.SDL_QUIT then
+    return false
+  if eventType == 0 then
+    IO.sleep 10
+  waitForCameraPermission
+
 structure WebcamState where
   window : SDL.SDLWindow
   renderer : SDL.SDLRenderer
@@ -86,6 +98,12 @@ def main : IO Unit := do
   let idx := cameraCount[0]!
   let camera ← SDL.openCamera idx
 
+  IO.println "Waiting for camera permission..."
+  unless (← waitForCameraPermission) do
+    IO.println "Camera permission denied"
+    SDL.quit
+    return
+
   let spec ← SDL.getCameraFormat camera
 
   let msg :=

justfile

@@ -1,3 +1,6 @@
+# Lean runs `main` on a helper thread by default; Cocoa only creates a video device on the main thread.
+export LEAN_MAIN_USE_THREAD := if os() == "macos" { "0" } else { "1" }
+
 _default:
     @just --list