Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move infoview to JavaScript modules #151

Merged
merged 29 commits into from
Mar 22, 2022
Merged

Conversation

Vtec234
Copy link
Member

@Vtec234 Vtec234 commented Mar 9, 2022

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
Copy link
Contributor

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

image

@Vtec234
Copy link
Member Author

Vtec234 commented Mar 9, 2022

@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
Copy link
Contributor

lovettchris commented Mar 9, 2022

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

image

@Vtec234
Copy link
Member Author

Vtec234 commented Mar 9, 2022

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

@lovettchris
Copy link
Contributor

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:

image

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

@gebner
Copy link
Member

gebner commented Mar 9, 2022

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 Vtec234 marked this pull request as ready for review March 18, 2022 02:43
@Vtec234
Copy link
Member Author

Vtec234 commented Mar 18, 2022

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.

lean4-infoview/README.md Show resolved Hide resolved
vscode-lean4/webpack.config.js Show resolved Hide resolved
lean4-infoview/package.json Show resolved Hide resolved
@gebner
Copy link
Member

gebner commented Mar 18, 2022

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
Copy link
Member

gebner commented Mar 18, 2022

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
Copy link
Member

gebner commented Mar 18, 2022

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
}]

@gebner gebner closed this Mar 18, 2022
@gebner gebner reopened this Mar 18, 2022
@Vtec234
Copy link
Member Author

Vtec234 commented Mar 20, 2022

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

@Vtec234
Copy link
Member Author

Vtec234 commented Mar 20, 2022

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

I am not seeing this.

@gebner
Copy link
Member

gebner commented Mar 21, 2022

I am not seeing this.

Can't reproduce it either now.

@gebner
Copy link
Member

gebner commented Mar 21, 2022

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

@Vtec234
Copy link
Member Author

Vtec234 commented Mar 21, 2022

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

Yep!

@lovettchris
Copy link
Contributor

@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
Copy link
Member

Kha commented Mar 21, 2022

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
Copy link
Contributor

lovettchris commented Mar 21, 2022

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

@Kha
Copy link
Member

Kha commented Mar 21, 2022

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
Copy link
Contributor

lovettchris commented Mar 21, 2022

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
Copy link
Contributor

lovettchris commented Mar 21, 2022

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
Copy link
Member Author

Vtec234 commented Mar 21, 2022

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
Copy link
Contributor

lovettchris commented Mar 22, 2022

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:
image

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

@lovettchris
Copy link
Contributor

Cool, the windows tests pass now!

@lovettchris
Copy link
Contributor

lovettchris commented Mar 22, 2022

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
Copy link
Member Author

Vtec234 commented Mar 22, 2022

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

Yes, they run and pass locally for me.

@Kha
Copy link
Member

Kha commented Mar 22, 2022

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
Copy link
Contributor

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

@lovettchris
Copy link
Contributor

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
Copy link
Member Author

Vtec234 commented Mar 22, 2022

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.

@Vtec234 Vtec234 merged commit 46a0219 into leanprover:master Mar 22, 2022
@Vtec234 Vtec234 deleted the infoview-hooks branch March 23, 2022 00:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants