# This is run when starting a Gitpod workspace on this repository

image: leanprovercommunity/gitpod4

vscode:
  extensions:
    - leanprover.lean4 # install the Lean 4 VS Code extension

tasks:
  - init: |
      elan self update
      lake exe cache get