Testing out widgets

Stream: lean4

[Tomas Skrivan]

I just had a moment to try out widgets while traveling. First of all, amazing work! However, I got into few troubles while reading the doc.

1. It is not explained what "RPC method" is. What does the RPC stand for?
2. When I copy paste the code snippets the formatting is all messed up. For example copy pasting the getType method to VS Code I get

open Server RequestM in
@[serverRpcMethod]
def
getType (
params :
GetTypeParams) :
RequestM (
RequestTask
CodeWithInfos)
...

3. When building the rubiks cube example I got an error the following error. I have zero experience with web development, so it is gibberish to me.

error: > npm run build -- --tsxName rubiks    # in directory ./widget
error: stdout:

> rubiks-cube@1.0.0 build /home/tomass/Documents/lean4-samples/RubiksCube/widget
> rollup --environment NODE_ENV:production --config "--tsxName" "rubiks"
error: stderr:
sh: 1: rollup: not found
npm ERR! code ELIFECYCLE
npm ERR! syscall spawn
npm ERR! file sh
npm ERR! errno ENOENT
npm ERR! rubiks-cube@1.0.0 build: `rollup --environment NODE_ENV:production --config "--tsxName" "rubiks"`
npm ERR! spawn ENOENT
npm ERR!
npm ERR! Failed at the rubiks-cube@1.0.0 build script.
npm ERR! This is probably not a problem with npm. There is likely additional logging output above.

npm ERR! A complete log of this run can be found in:
npm ERR!     /home/tomass/.npm/_logs/2022-08-11T23_53_44_208Z-debug.log
error: external command `npm` exited with code 1

[Mario Carneiro]

RPC stands for "remote procedure call". It's basically a way for a program running inside VSCode to directly call a function inside the lean executable (or vice versa)

[Chris Lovett]

Check your npm versions, this is what I'm using:

(base) chris@clovett15:~/git/lean4-samples/RubiksCube/widget$ npm --version
8.5.5
(base) chris@clovett15:~/git/lean4-samples/RubiksCube/widget$ node --version
v16.15.0

then I do this:

cd widget
npm install
cd ..
lake build rubiksJs
lake build
code .

If you are on Windows you may need some other fixes I'm working on.

[Wojciech Nawrocki]

When I copy paste the code snippets the formatting is all messed up. For example copy pasting the getType method to VS Code I get

Ah that's unfortunate. The tutorial is compiled from a literate Lean file here, we should probably link it from the leanink html. (CC @Sebastian Ullrich )

[Wojciech Nawrocki]

When building the rubiks cube example I got an error the following error. I have zero experience with web development, so it is gibberish to me

It looks like the widget build forgot to install its dependencies. As Chris says, you may have an old Node.js version or something, but it's hard to say. However you should not have to run all these steps yourself. The following two steps suffice for me on a fresh clone:

lake build rubiksJs
code Rubiks.lean

If these don't suffice, it's a bug I'd say.

[Sebastian Ullrich]

Wojciech Nawrocki said:

When I copy paste the code snippets the formatting is all messed up. For example copy pasting the getType method to VS Code I get

Ah that's unfortunate. The tutorial is compiled from a literate Lean file here, we should probably link it from the leanink html. (CC Sebastian Ullrich )

We can do that, would be even better to fix this in LeanInk though

[Wojciech Nawrocki]

It is not explained what "RPC method" is. What does the RPC stand for?

The acronym is now expanded in the tutorial.

[Tomas Skrivan]

Wojciech Nawrocki said:

When building the rubiks cube example I got an error the following error. I have zero experience with web development, so it is gibberish to me

It looks like the widget build forgot to install its dependencies. As Chris says, you may have an old Node.js version or something, but it's hard to say. However you should not have to run all these steps yourself. The following two steps suffice for me on a fresh clone:

lake build rubiksJs
code Rubiks.lean

If these don't suffice, it's a bug I'd say.

This unfortunately does not work for me.

I have npm --version = 6.14.4 and nodejs --version = v10.19.0. I guess these are default versions on Ubuuntu 20.04. Do I need to upgrade? (I have tried few upgrade commands from stack exchange but without success yet)

[Wojciech Nawrocki]

Tomas Skrivan said:

Wojciech Nawrocki said:

When building the rubiks cube example I got an error the following error. I have zero experience with web development, so it is gibberish to me

It looks like the widget build forgot to install its dependencies. As Chris says, you may have an old Node.js version or something, but it's hard to say. However you should not have to run all these steps yourself. The following two steps suffice for me on a fresh clone:

lake build rubiksJs
code Rubiks.lean

If these don't suffice, it's a bug I'd say.

This unfortunately does not work for me.

I have npm --version = 6.14.4 and nodejs --version = v10.19.0. I guess these are default versions on Ubuuntu 20.04. Do I need to upgrade? (I have tried few upgrade commands from stack exchange but without success yet)

I see, these are very old versions. I can't say for sure that this will solve the issue but it's definitely worth trying a newer one. A good user-directory installation method is nvm, it'll pull something newer than your distro's version. It works basically like elan.

[Tomas Skrivan]

Great, got it working now. It is super cool!