feat: rubiks cube sample

RubiksCube/.gitignore

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

RubiksCube/README.md

@@ -0,0 +1,16 @@
+# Rubiks cube visualiser
+
+This project is a demo for showing rubiks cubes in the lean infoview.
+Inspired by the [rubiks-cube-group](https://github.com/kendfrey/rubiks-cube-group) by Kendal Frey.
+
+## Building
+
+In order to install you need [Lean](https://leanprover.github.io/lean4/doc/quickstart.html) and [npm](https://npmjs.com).
+You also need to be using VSCode (or a gitpod).
+
+```
+cd widget
+npm i
+cd ..
+lake build
+```

RubiksCube/Rubiks.lean

@@ -0,0 +1,21 @@
+import Lean
+open Lean Elab
+
+elab (name := includeStr) "include_str " str:str : term => do
+  let some str := str.isStrLit? | Lean.Elab.throwUnsupportedSyntax
+  let ctx ← readThe Lean.Core.Context
+  let srcPath := System.FilePath.mk ctx.fileName
+  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
+  let path := srcDir / str
+  Lean.mkStrLit <$> IO.FS.readFile path
+
+@[widgetSource]
+def rubiks : String := include_str "./widget/dist/rubiks.js"
+
+structure RubiksProps where
+  seq : Array String := #[]
+  deriving ToJson, FromJson, Inhabited
+
+def eg : RubiksProps := {seq := #["U", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"]}
+
+#widget rubiks (toJson eg)

RubiksCube/lakefile.lean

@@ -0,0 +1,23 @@
+import Lake
+open System Lake DSL
+
+def jsTarget (pkgDir : FilePath) : FileTarget :=
+  let jsFile := pkgDir / "widget/dist/rubiks.js"
+  let srcFiles := inputFileTarget <| pkgDir / "widget/src/rubiks.tsx"
+  fileTargetWithDep jsFile srcFiles fun _srcFile => do
+    proc {
+      cmd := "npm"
+      args := #["install"]
+      cwd := some <| pkgDir / "widget"
+    }
+    proc {
+      cmd := "npm"
+      args := #["run", "build"]
+      cwd := some <| pkgDir / "widget"
+    }
+
+package Rubiks (pkgDir) {
+  extraDepTarget := jsTarget pkgDir |>.withoutInfo
+  defaultFacet := PackageFacet.oleans
+  dependencies := #[ ]
+}

RubiksCube/lean-toolchain

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