feat: rubiks cube sample

README.md

@@ -18,3 +18,9 @@ Explore more standard input processing with a [simple guess-my-number game](Gues
 ## CSV Parser
 
 [CSV parser](CSVParser/README.md) is the simplest practical CSV parser you can write in Lean.
+
+## Rubik's cube
+
+[Rubik's cube](RubiksCube/README.md) is an example showing how to build custom [user widgets](https://leanprover.github.io/lean4/doc/examples/widgets.lean.html)
+for the InfoView using TypeScript and Lake. Given a sequence of moves, it renders a Rubik's cube
+in 3D which can be animated with the movement of a slider.

RubiksCube/.gitignore

@@ -0,0 +1,4 @@
+build
+widget/dist
+widget/node_modules
+.vscode/

RubiksCube/README.md

@@ -0,0 +1,20 @@
+![A screenshot showing the Rubik's cube in operation.](./images/screenshot.png)
+
+# Rubik's cube visualiser
+
+This project is a demo of the user widgets system. It displays a Rubik's cube in the Lean infoview.
+Inspired by the [rubiks-cube-group](https://github.com/kendfrey/rubiks-cube-group) from Kendal Frey.
+
+The purpose of this example is to show how to build widgets using TypeScript and bundled NPM libraries.
+
+## Running
+
+In order to build you need [Lean 4](https://leanprover.github.io/lean4/doc/quickstart.html)
+and [Node.js](https://nodejs.org/en/). You also need to be using VSCode (or a Gitpod). First run
+
+```shell
+lake build rubiksJs
+```
+
+and then open `Rubiks.lean` in the editor. Put your cursor over the `#widget` command and you should
+see an interactive Rubik's cube in the infoview.

RubiksCube/Rubiks.lean

@@ -0,0 +1,16 @@
+import Lean
+open Lean Elab Widget
+
+@[widget]
+def rubiks : UserWidgetDefinition := {
+  name := "Rubik's cube"
+  javascript:= include_str "widget" / "dist" / "rubiks.js"
+}
+
+structure RubiksProps where
+  seq : Array String := #[]
+  deriving ToJson, FromJson, Inhabited
+
+def eg : RubiksProps := {seq := #["L", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"]}
+
+#widget rubiks (toJson eg)

RubiksCube/lakefile.lean

@@ -0,0 +1,41 @@
+import Lake
+open System Lake DSL
+
+package Rubiks
+
+def npmCmd : String :=
+  if Platform.isWindows then "npm.cmd" else "npm"
+
+target packageLock : FilePath := do
+  let widgetDir := __dir__ / "widget"
+  let packageFile ← inputFile <| widgetDir / "package.json"
+  let packageLockFile := widgetDir / "package-lock.json"
+  buildFileAfterDep packageLockFile packageFile fun _srcFile => do
+    proc {
+      cmd := npmCmd
+      args := #["install"]
+      cwd := some widgetDir
+    }
+
+def tsxTarget (pkg : Package) (tsxName : String) [Fact (pkg.name = _package.name)]
+    : IndexBuildM (BuildJob FilePath) := do
+  let widgetDir := __dir__ / "widget"
+  let jsFile := widgetDir / "dist" / s!"{tsxName}.js"
+  let deps : Array (BuildJob FilePath) := #[
+    ← inputFile <| widgetDir / "src" / s!"{tsxName}.tsx",
+    ← inputFile <| widgetDir / "rollup.config.js",
+    ← inputFile <| widgetDir / "tsconfig.json",
+    ← fetch (pkg.target ``packageLock)
+  ]
+  buildFileAfterDepArray jsFile deps fun _srcFile => do
+    proc {
+      cmd := npmCmd
+      args := #["run", "build", "--", "--tsxName", tsxName]
+      cwd := some widgetDir
+    }
+
+target rubiksJs (pkg : Package) : FilePath := tsxTarget pkg "rubiks"
+
+-- TODO: https://github.com/leanprover/lake/issues/86#issuecomment-1185028364
+@[defaultTarget]
+lean_lib Rubiks

RubiksCube/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2022-08-08