Infoview does not load (ARM64)

[PDeets]

Hello, I just installed the VS code lean4 extension, but the "Lean Infoview" is blank. I am using an ARM64 build of Windows 11, but I have the x64 build of Lean installed and am able to build and run lean programs in the VS Code terminal. The "Lean documentation" works, but not the infoview.

Do you have any suggestions for how to debug this? (I am a programmer, but my expertise is in C++. I'm not familiar with React.)

Here is a screenshot:

[Vtec234]

Hi! One thing you could try would be to run Developer: Toggle Developer Tools from the command panel and paste the contents of the Console tab here (using <details> to avoid a huge message). Then we can look for anything suspicious there.

[PDeets]

I don't see any obvious issues in the output, but here it is:

INFO Electron sandbox mode is enabled! log.ts:398 WARN Via 'product.json#extensionEnabledApiProposals' extension 'github.vscode-pull-request-github' wants API proposal 'commentsResolvedState' but that proposal DOES NOT EXIST. Likely, the proposal has been finalized (check 'vscode.d.ts') or was abandoned. console.ts:137 [Extension Host] 00:15:26.080 - executeWithProgress lean +leanprover/lean4:nightly,--version localProcessExtensionHost.ts:298 Extension Host localProcessExtensionHost.ts:299 00:15:26.080 - executeWithProgress lean +leanprover/lean4:nightly,--version

log.ts:392 INFO [perf] Render performance baseline is 45ms console.ts:137 [Extension Host] 00:15:29.151 - [LeanInstaller] lean returned: Lean (version 4.0.0-nightly-2023-02-24, commit 473486eeb9bc, Release) console.ts:137 [Extension Host] 00:15:29.164 - child process exited with code 0 localProcessExtensionHost.ts:298 Extension Host localProcessExtensionHost.ts:299 00:15:29.151 - [LeanInstaller] lean returned: Lean (version 4.0.0-nightly-2023-02-24, commit 473486eeb9bc, Release) 00:15:29.164 - child process exited with code 0

console.ts:137 [Extension Host] 00:15:29.283 - [LeanInstaller] elan returned: elan 1.4.2 (4a1b1b918 2022-09-13) console.ts:137 [Extension Host] 00:15:29.284 - [LeanInstaller] elan returned: console.ts:137 [Extension Host] 00:15:29.289 - child process exited with code 0 console.ts:137 [Extension Host] 00:15:29.372 - child process exited with code 0 console.ts:137 [Extension Host] 00:15:29.372 - [ClientProvider] Creating LeanClient for file:///c%3A/Users/pdeet/source/Lean console.ts:137 [Extension Host] 00:15:29.373 - [ClientProvider] firing clientAddedEmitter event console.ts:137 [Extension Host] 00:15:29.373 - [InfoProvider] Adding client for workspace: file:///c%3A/Users/pdeet/source/Lean console.ts:137 [Extension Host] 00:15:29.374 - [LeanClient] Restarting Lean Server console.ts:137 [Extension Host] 00:15:29.378 - [LeanClient] starting localProcessExtensionHost.ts:298 Extension Host localProcessExtensionHost.ts:299 00:15:29.283 - [LeanInstaller] elan returned: elan 1.4.2 (4a1b1b918 2022-09-13) 00:15:29.284 - [LeanInstaller] elan returned: 00:15:29.289 - child process exited with code 0 00:15:29.372 - child process exited with code 0 00:15:29.372 - [ClientProvider] Creating LeanClient for file:///c%3A/Users/pdeet/source/Lean 00:15:29.373 - [ClientProvider] firing clientAddedEmitter event 00:15:29.373 - [InfoProvider] Adding client for workspace: file:///c%3A/Users/pdeet/source/Lean 00:15:29.374 - [LeanClient] Restarting Lean Server 00:15:29.378 - [LeanClient] starting

console.ts:137 [Extension Host] 00:15:35.000 - [LeanClient] running, started in 5626 ms console.ts:137 [Extension Host] 00:15:35.005 - [InfoProvider] got client restarted event console.ts:137 [Extension Host] 00:15:35.006 - [InfoProvider] initInfoView! localProcessExtensionHost.ts:298 Extension Host localProcessExtensionHost.ts:299 00:15:35.000 - [LeanClient] running, started in 5626 ms 00:15:35.005 - [InfoProvider] got client restarted event 00:15:35.006 - [InfoProvider] initInfoView!

[mhuisi]

@PDeets Hey, did you eventually manage to get the infoview working?

[PDeets]

I did not get it to work on my Windows ARM64 device. (It is a Windows Dev Kit 2023.) What I eventually did is buy a new computer with an Intel processor. It worked fine on the computer with the Intel processor.

[mhuisi]

Thanks! I assume the new computer is also a Windows 11 machine?

[PDeets]

Yes, that is correct. The new computer where it worked is an HP Omen laptop running Windows 11.