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.
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:
I tried running the terminal (bash shell) command
in both the current directory, or after
cd RubiksCube
, but either way I get the messageEntering:
and clicking on the #widget command brought up the Rubik's cube widget for me.