`widget_module` で p5js を使用するウィジェットを自作する

ProofWidgets4 の作者に教えていただいた例

import Lean

open Lean Widget

@[widget_module]
def P5Widget : Widget.Module where
  javascript := "
    import * as React from 'react'
    import p5 from 'https://esm.sh/p5'

    function sketch(p5) {
      p5.setup = () => {
        p5.createCanvas(600, 400, p5.WEBGL);
      };
      
      p5.draw = () => {
        p5.background(250);
        p5.normalMaterial();
        p5.push();
        p5.rotateZ(p5.frameCount * 0.01);
        p5.rotateX(p5.frameCount * 0.01);
        p5.rotateY(p5.frameCount * 0.01);
        p5.plane(100);
        p5.pop();
      };
    }

    export default function() {
      React.useEffect(() => {
        new p5(sketch, 'p5sketch')
      }, [])
      return React.createElement('div', { id: 'p5sketch' })
    }
    "
  
#widget P5Widget

Start by locating where Lean widget examples are stored and how widget_module examples are presented. Review the issue's P5Widget snippet and verify whether the repository should include it as a runnable example; done means the p5js-based widget can be found and used successfully.