Move infoview to JavaScript modules

[Vtec234]

We move the infoview to be a JavaScript module rather than a UMD library. This will allow us to dynamically import widget modules provided by the Lean server and provide them with the same version of React that we use, as well as core UI components such as interactive expressions.

• Clarify infoview documentation. @lean4/infoview is now becoming something that is to be imported both by the webview in order to call renderInfoview, as well as by custom widgets in order to use interactive expressions, messages, etc. We may want to split these functionalities into two packages eventually, but for now I think this is okay as long as it's explained.
• The webpack CopyPlugin in vscode-lean4 doesn't seem to propagate changes to the infoview on npm run watch properly.
• @lovettchris Could you please check whether the infoview debugging setup still works? This PR changes the code generation quite a bit.

/CC @EdAyers

[lovettchris]

@Vtec234 - have the build steps changed? I get this error:

[Vtec234]

@lovettchris Nope, they are still npm install; npx lerna bootstrap; npx lerna run build at the top level. I just tried again and it works on Linux. Could you please try with a fresh clone? If it fails, it might is a Windows-specific problem. EDIT: Oh, what is your npm --version and node --version? This might also be something that requires recent Node.js.

[lovettchris]

Perhaps your rollup calls are missing --configPlugin typescript ? This gets further but this this error:

[Vtec234]

Nope, the rollup.config.js is JavaScript, it does not need the TS plugin.

[lovettchris]

I tried again starting with git clean -dfx on your branch, followed by npm install, then npx lerna bootstrap and then npx lerna run build and the build fails:

Looks like we need to setup a CI build on a Windows machine.

[gebner]

AFAICT, you need to import {React} from '@lean4/infoview' now to get react. I guess this won't work with libraries like react-d3-library, etc. Is there a way to make import * as React from 'react' work, so that you can use it as a peer dependency?

[Vtec234]

This is ready to review. I still can't get CopyPlugin to update the files when lean4-infoview is recompiled in watch mode. It might be a bug in the plugin but I do not have the energy to investigate that.

[gebner]

The webpack CopyPlugin in vscode-lean4 doesn't seem to propagate changes to the infoview on npm run watch properly.

Possibly related to this: webpack-contrib/copy-webpack-plugin#674

This is moderately annoying a blocker, can we add a hack to fix this like directly load node_modules/@lean4/infoview/... in dev mode?

[gebner]

There's also this new warning which we should suppress (preferably by turning eval into new Function I guess).

@lean4/infoview: (!) Use of eval is strongly discouraged
@lean4/infoview: https://rollupjs.org/guide/en/#avoiding-eval
@lean4/infoview: src/infoview/main.tsx
@lean4/infoview: 78:         requestedAction: async (action) => editorEvents.requestedAction.fire(action),
@lean4/infoview: 79:         // eslint-disable-next-line no-eval
@lean4/infoview: 80:         runTestScript: async (script) => eval(script),
@lean4/infoview:                                              ^
@lean4/infoview: 81:         getInfoviewHtml: async () => document.body.innerHTML,
@lean4/infoview: 82:     };

[gebner]

I'm also getting another (new?) warning:

[{
	"resource": "/home/gebner/vscode-lean4/lean4-infoview/src/infoview/main.tsx",
	"owner": "eslint",
	"code": {
		"value": "@typescript-eslint/no-unsafe-argument",
		"target": "..."
	},
	"severity": 8,
	"message": "Unsafe argument of type `any` assigned to a parameter of type `string`.",
	"source": "eslint",
	"startLineNumber": 118,
	"startColumn": 45,
	"endLineNumber": 118,
	"endColumn": 51
}]

[Vtec234]

All should work now, CopyPlugin turned out to be a documented bad interaction with monorepos.

[Vtec234]

I'm also getting another (new?) warning:

I am not seeing this.

[gebner]

I am not seeing this.

Can't reproduce it either now.

[gebner]

Did you test whether installing and running the extension from the packaged vsix still works?

[Vtec234]

Did you test whether installing and running the extension from the packaged vsix still works?

Yep!

[lovettchris]

@Vtec234 - the CI failure you see here is due to a change I'm making to how windows elan-init.ps1 works (so there is no prompt when all goes well). See leanprover/elan#63. So we need to get my matching PR #157 in ASAP and then when you merge that fix your PR will be good.

[Kha]

Wait, so did we break the interface of the installer file used on e.g. https://leanprover.github.io/lean4/doc/quickstart.html? Could we please not do that?

[lovettchris]

@Kha The quickstart content is out of date. Leo needs to push the updates checked in with PR leanprover/lean4#842

[Kha]

Weird, I'll have to check why it didn't update automatically. But I'm still not okay with simply breaking the interface of previous versions of the script and on other platforms, especially if internally they are translated back to the original interface anyway. If all this was for PromptOnError, surely this can be done in vscode-lean4 as well just like on Unix instead of making the platforms drift further apart?

[lovettchris]

But I'm still not okay with simply breaking the interface of previous versions of the script and on other platforms, especially if internally they are translated back to the original interface anyway. If all this was for PromptOnError, surely this can be done in vscode-lean4 as well just like on Unix instead of making the platforms drift further apart?

I would agree if all platforms were using the same scripting language. But PowerShell is different, it has a different parameter parsing rules and I claim my change is more consistent with that. But I can remove the "-PromptOnError" since the linux script does not support that concept, and move it back to the vscode extension if this is what you prefer. But the syntax differences of powershell parameters "-DefaultToolchain" versus "--default-toolchain" should remain IMHO.

[lovettchris]

Weird, I'll have to check why it didn't update automatically.

Currently Leo has to run deploy.sh in TPIL to push to gh-pages. I asked Leo if he wanted an automated CI workflow to do that and he said no. I pinged him on Zulip to remind him to do it.

[Vtec234]

Since the CI failure is unrelated to the content of this PR, I think it would be okay to just merge it now assuming there are no further comments?

EDIT: @lovettchris I think you accidentally put your response in my message by editing it :) Here is the response:

Please don't I want to see your PR pass on Windows first. So please merge #157 first, it's ready now, thanks.

[lovettchris]

Since the CI failure is unrelated to the content of this PR, I think it would be okay to just merge it now assuming there are no further comments?

EDIT: @lovettchris I think you accidentally put your response in my message by editing it :) Here is the response:

Please don't I want to see your PR pass on Windows first. So please merge #157 first, it's ready now, thanks.

Sorry about the edit, weird that github let me do that. The re-run passed:

oh, and I see #157 is merged. Thanks.

[lovettchris]

Cool, the windows tests pass now!

[lovettchris]

Hmmm they passed on the CI build machine, but they still fail on my devbox with this error. Can you run the tests manually in vscode using the "Extension Tests - *" launch configurations?

TypeError: Cannot read property 'describe' of undefined

and when I try and run a test in VS code it says something else:

Error: Cannot find module 'd:\Temp\vtec234\vscode-lean4\vscode-lean4\out\test\suite\lean3'
Require stack:
- c:\Users\clovett\AppData\Local\Programs\Microsoft VS Code\resources\app\out\vs\loader.js
- c:\Users\clovett\AppData\Local\Programs\Microsoft VS Code\resources\app\out\bootstrap-amd.js
- c:\Users\clovett\AppData\Local\Programs\Microsoft VS Code\resources\app\out\bootstrap-fork.js
    at Function._resolveFilename (<node_internals>/internal/modules/cjs/loader.js:934:15)
    at <node_internals>/internal/modules/cjs/loader.js:779:27
    at Function.<anonymous> (<node_internals>/electron/js2c/asar_bundle.js:5:12913)

this will be a huge productivity problem for me if we can't get it working smoothly.

[Vtec234]

Can you run the tests manually in vscode using the "Extension Tests - *" launch configurations?

Yes, they run and pass locally for me.

[Kha]

But I'm still not okay with simply breaking the interface of previous versions of the script and on other platforms, especially if internally they are translated back to the original interface anyway. If all this was for PromptOnError, surely this can be done in vscode-lean4 as well just like on Unix instead of making the platforms drift further apart?

I would agree if all platforms were using the same scripting language. But PowerShell is different, it has a different parameter parsing rules and I claim my change is more consistent with that. But I can remove the "-PromptOnError" since the linux script does not support that concept, and move it back to the vscode extension if this is what you prefer. But the syntax differences of powershell parameters "-DefaultToolchain" versus "--default-toolchain" should remain IMHO.

The parameters come from the elan-init binary, that's not a scripting language. It still looks like unnecessary churn to me given that it worked fine before, but if we're changing that, let's do it the right way: there is an unexposed flag --no-modify-path, and the default for default-toolchain is stable, not none (but that shouldn't be hard-coded, the flag simply shouldn't be passed by default) https://github.com/leanprover/elan/blob/master/src/elan-cli/setup_mode.rs

[lovettchris]

Ok @Kha, I'll move this discussion to Zulip since it is unrelated to this PR

[lovettchris]

Can you run the tests manually in vscode using the "Extension Tests - *" launch configurations?

Yes, they run and pass locally for me.

On Linux? And that's with vscode and not with "npm run tests" ?

[Vtec234]

On Linux? And that's with vscode and not with "npm run tests" ?

Yup to both. npm run test also works for me.

I'll merge this now as much of the discussion has lost its relevance to the PR itself, if there are remaining dev setup issues let's fix them in followup PRs.