search

leanprover-community / lean4-samples

Code samples for Lean 4
Apache License 2.0
67 stars 22 forks source link

feat: rubiks cube sample #3

Closed EdAyers closed 1 year ago

EdAyers commented 2 years ago

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

Tasks

Vtec234 commented 1 year ago

@lovettchris this should be ready for review and testing.

lovettchris commented 1 year ago

@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 commented 1 year ago

@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 commented 1 year ago

@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 commented 1 year ago

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 commented 1 year ago

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

image

I also filed this new bug against lean as a reminder to complete that open PR: https://github.com/leanprover/lean4/issues/1410

lovettchris commented 1 year ago

Seems to work great on Linux though:

image

lovettchris commented 1 year ago

I also verified that https://github.com/leanprover/lean4/pull/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.

image

lovettchris commented 1 year ago

@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 commented 1 year ago

@leodemoura could the include_str macro live in core?

leodemoura commented 1 year ago

@leodemoura could the include_str macro live in core?

Yes!

EdAyers commented 1 year ago

Added here: https://github.com/leanprover/lean4/pull/1407/commits/98513fa5d6de602964167a6ebb9a6ebb571d2747