Testing the vs-code extension

Stream: general

[Eric Wieser]

I want to try and edit the vs-code extension, but when I check it out in vs-code and hit F5, I get this error traceback:

> Executing task: npm run compile <


> lean@0.16.17 compile C:\Users\wiese\Repos\lean\vscode-lean
> webpack --env.development

Hash: 3e3830c841fb123b8e282d197da4855fcbd1905c
Version: webpack 4.43.0
Child webview:
    Hash: 3e3830c841fb123b8e28
    Time: 24849ms
    Built at: 01/01/2021 20:14:11
       Asset      Size  Chunks             Chunk Names
    index.js  3.21 MiB   index  [emitted]  index
    Entrypoint index = index.js
    [./infoview/collapsing.tsx] 1.67 KiB {index} [built]
    [./infoview/goal.tsx] 2.09 KiB {index} [built]
    [./infoview/index.css] 1.13 KiB {index} [built]
    [./infoview/index.tsx] 6.01 KiB {index} [built]
    [./infoview/info.tsx] 10.5 KiB {index} [built]
    [./infoview/messages.tsx] 4.53 KiB {index} [built]
    [./infoview/server.ts] 5.66 KiB {index} [built]
    [./infoview/svg_icons.tsx] 3.92 KiB {index} [built]
    [./infoview/tachyons.css] 1.13 KiB {index} [built]
    [./infoview/util.tsx] 1.31 KiB {index} [built]
    [./infoview/widget.tsx] 8.68 KiB {index} [built] [1 error]
    [./media/copy-to-comment-light.svg] 493 bytes {index} [built]
    [./node_modules/css-loader/dist/cjs.js!./infoview/index.css] 1.98 KiB {index} [built]
    [./node_modules/css-loader/dist/cjs.js!./infoview/tachyons.css] 119 KiB {index} [built]
    [./src/shared.ts] 551 bytes {index} [built]
        + 81 hidden modules

    ERROR in ./infoview/widget.tsx
    Module not found: Error: Can't resolve 'katex/dist/katex.min.css' in 'C:\Users\wiese\Repos\lean\vscode-lean\infoview'
     @ ./infoview/widget.tsx 20:0-35
     @ ./infoview/info.tsx
     @ ./infoview/index.tsx

    ERROR in ./infoview/widget.tsx
    Module not found: Error: Can't resolve 'react-katex' in 'C:\Users\wiese\Repos\lean\vscode-lean\infoview'
     @ ./infoview/widget.tsx 21:14-36
     @ ./infoview/info.tsx
     @ ./infoview/index.tsx

    ERROR in C:\Users\wiese\Repos\lean\vscode-lean\infoview\widget.tsx
    ./infoview/widget.tsx
    [tsl] ERROR in C:\Users\wiese\Repos\lean\vscode-lean\infoview\widget.tsx(9,24)
          TS2307: Cannot find module 'react-katex' or its corresponding type declarations.
Child extension:
    Hash: 2d197da4855fcbd1905c
    Time: 28464ms
    Built at: 01/01/2021 20:14:15
               Asset      Size     Chunks                   Chunk Names
        extension.js  2.45 MiB  extension  [emitted]        extension
    extension.js.map  2.17 MiB  extension  [emitted] [dev]  extension
    Entrypoint extension = extension.js extension.js.map
    [./src/batch.ts] 1.06 KiB {extension} [built]
    [./src/completion.ts] 3.85 KiB {extension} [built]
    [./src/definition.ts] 1.59 KiB {extension} [built]
    [./src/diagnostics.ts] 2.51 KiB {extension} [built]
    [./src/docview.ts] 11.6 KiB {extension} [built]
    [./src/extension.ts] 5.58 KiB {extension} [built]
    [./src/holes.ts] 4.42 KiB {extension} [built]
    [./src/hover.ts] 2.43 KiB {extension} [built]
    [./src/infoview.ts] 16.8 KiB {extension} [built]
    [./src/input.ts] 14.1 KiB {extension} [built]
    [./src/leanpkg.ts] 7.25 KiB {extension} [built]
    [./src/librarynote.ts] 2.24 KiB {extension} [built]
    [./src/roi.ts] 7.21 KiB {extension} [built]
    [./src/search.ts] 1.65 KiB {extension} [built]
    [./src/server.ts] 9.56 KiB {extension} [built]
        + 573 hidden modules

    WARNING in ./node_modules/express/lib/view.js 81:13-25
    Critical dependency: the request of a dependency is an expression
     @ ./node_modules/express/lib/application.js
     @ ./node_modules/express/lib/express.js
     @ ./node_modules/express/index.js
     @ ./src/staticserver.ts
     @ ./src/extension.ts
npm ERR! code ELIFECYCLE
npm ERR! errno 2
npm ERR! lean@0.16.17 compile: `webpack --env.development`
npm ERR! Exit status 2
npm ERR!
npm ERR! Failed at the lean@0.16.17 compile 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!     C:\Users\wiese\AppData\Roaming\npm-cache\_logs\2021-01-01T20_14_15_808Z-debug.log
The terminal process "C:\Program Files\Git\bin\bash.exe '-c', 'npm run compile'" terminated with exit code: 2.

Am I missing a development step?

[Eric Wieser]

Ah, I guess I need to rerun npm install