feat: rubiks cube sample

[EdAyers]

This PR includes a minimal example of user widgets and a more involved rubiks cube example

Tasks

• feat: user widgets leanprover/vscode-lean4#194
• feat: user widgets leanprover/lean4#1238
• add an example RPC call to WidgetsMinimal
• update lean-toolchain
• move include_str to utility file or put in core?

[lovettchris]

This doesn't work on windows, perhaps this would be better:

  let jsFile := pkgDir / "widget" / "dist" / "rubiks.js"
  let srcFiles := inputFileTarget <| pkgDir / "widget" / "src" / "rubiks.tsx"

[lovettchris]

Ah, the proposed change is good, but we also need this fix in lean for it to work: leanprover/lean4#1257

[Vtec234]

@lovettchris this should be ready for review and testing.

[lovettchris]

@lovettchris this should be ready for review and testing.

LEAN_PATH=.\build\lib c:\Users\clovett.elan\toolchains\leanprover--lean4---nightly-2022-08-01\bin\lean.exe ...\Rubiks.lean -R ... -o .\build\lib\Rubiks.olean -i .\build\lib\Rubiks.ilean -c .\build\ir\Rubiks.c
error: stdout:
...\Rubiks.lean:16:15: error: no such file or directory (error code: 2)
file: ..../widget/dist/rubiks.js
...\Rubiks.lean:13:2: error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors
error: external command c:\Users\clovett.elan\toolchains\leanprover--lean4---nightly-2022-08-01\bin\lean.exe exited with status 1
error: build failed

[Vtec234]

@lovettchris unfortunately we are blocked on leanprover/lean4#2762 and this error will likely come up again. However please see the updated README.md - the new instructions are to run lake build rubiksJs first.

[lovettchris]

@lovettchris unfortunately we are blocked on leanprover/lean4#2762 and this error will likely come up again. However please see the updated README.md - the new instructions are to run lake build rubiksJs first.

lake build rubiksJs
> npm install    # in directory .\widget
error: no such file or directory (error code: 2)
error: build failed

I think the problem is that you are hard coding forward slashes in a string literal which results in an invalid path on Windows. Can you change include_str to take a System.FilePath so i can write this instead:

javascript:= include_str (System.FilePath.mk "." / "widget" / "dist" / "rubiks.js")

which generates the correct backslash path on Windows? We then seems to have one more bug in System.FilePath where it is generating a leading 'slash' in the combined path \d%3A\Temp\lean4-samples\RubiksCube\./widget/dist/rubiks.js - and that is also invalid on Windows. The string should be d:\Temp\lean4-samples\RubiksCube\.\widget\dist\rubiks.js... this seems to be a bug in Lean.Core.Context where ctx.fileName is returning the mangled path.

[Vtec234]

It looks like it's failing in the npm install step, long before the include_str has any relevance. We could definitely be more correct about paths, but fwiw forward-slash paths have always worked for me on modern versions of Windows. This looks a bit like leanprover/lean4#1257.

[lovettchris]

Could be related to that open issue, but it's definitely failing in the include_str, I see this in the editor:

I also filed this new bug against lean as a reminder to complete that open PR:
leanprover/lean4#1410

[lovettchris]

Seems to work great on Linux though:

[lovettchris]

I also verified that leanprover/lean4#1257 fixes the NPM build problem, but not the path problem, so I still see this in the editor (on Windows) after lake build rubiksJs has succeeded.

[lovettchris]

@EdAyers can you add a link and small blurb about the sample in the top level https://github.com/EdAyers/lean4-samples/blob/rubiks/README.md ?

[EdAyers]

@leodemoura could the include_str macro live in core?

[leodemoura]

@leodemoura could the include_str macro live in core?

Yes!

[EdAyers]

Added here: leanprover/lean4@98513fa