Rubik's cube with Gitpod needs extra shell commands to build

[crisperdue]

I have the Chrome Gitpod extension installed, and when I click on the Gitpod button
that appears on the page, it opens up a VSCode environment, showing the following
messages in the terminal window:

HISTFILE=/workspace/.gitpod/cmd-0 history -r; {
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly -y
echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.bashrc
echo '### You can now close this terminal and use use File/Open folder to open the sample you want to play with.'

}
gitpod /workspace/lean4-samples (main) $  HISTFILE=/workspace/.gitpod/cmd-0 history -r; {
> curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly -y
> echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.bashrc
> echo '### You can now close this terminal and use use File/Open folder to open the sample you want to play with.'
> 
> }
info: downloading installer
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-10-10
info: downloading component 'lean'
180.2 MiB / 180.2 MiB (100 %)  38.0 MiB/s ETA:   0 s                
info: installing component 'lean'
info: default toolchain set to 'leanprover/lean4:nightly'

  leanprover/lean4:nightly installed - Lean (version 4.0.0-nightly-2022-10-10, commit fb4200e63387, Release)

### You can now close this terminal and use use File/Open folder to open the sample you want to play with.
gitpod /workspace/lean4-samples (main) $

I tried running the terminal (bash shell) command

lake build rubiksJs

in both the current directory, or after cd RubiksCube, but either way I get the message

bash: lake: command not found

Entering:

. ~/.bashrc           # Execute the updated $HOME/.bashrc file
cd RubiksCube
lake build rubiksJs

and clicking on the #widget command brought up the Rubik's cube widget for me.

[besttea]

you should install elan.