Infoview hoverrendering missing css on firefox

[jcreedcmu]

This is the result of hovering over the natural numbers symbol.

What I expect: a nice opaque gray background.
What I observe: no background; transparent and illegible.

If I setTimeout(() => { debugger; }, 3000) in console and then hover, I can catch the state where the tooltip exists.

The css rule that should be applied here is from the infoview implementation https://github.com/leanprover/vscode-lean4/blob/bbe3ff126cd54defd10ac6e07a2b94dd2d865c42/lean4-infoview/src/infoview/index.css#L134-L148

document.querySelectorAll('link[rel="stylesheet"], style') shows that there is an active stylesheet, inside the iframe, with url

<link rel="stylesheet" href="https://vscode-remote%2Blocalhost-003a3000.vscode-resource.vscode-cdn.net/workspace/.openvscode-server/extensions/leanprover.lean4-universal/dist/lean4-infoview/index.css">

My guess is that this is a url that would work if we were in a genuine copy of vscode running on the desktop, and that something about openvscode-server or our configuration of it is failing to cause this url to be rewritten or resolve to the right thing.

[jcreedcmu]

Yeah, there's a clear error in the network tab where the infoview tries to load

https://vscode-remote+localhost-003a3000.vscode-resource.vscode-cdn.net/workspace/.openvscode-server/extensions/leanprover.lean4-universal/dist/lean4-infoview/index.css

but consistent success with all the js assets. Not sure why css is behaving differently.

[Vtec234]

The infoview CSS is on my list of things to address but feel free to get to it first!

[jcreedcmu]

Interestingly, I don't reproduce on chrome, and if I go into console and do

(await (await fetch("https://vscode-remote+localhost-003a3000.vscode-resource.vscode-cdn.net/workspace/.openvscode-server/extensions/leanprover.lean4-universal/dist/lean4-infoview/index.css")).text()).match(/\.tooltip.*/) 

I get Array [" .tooltip {" ] indicating that the fetch is successful.

So a theory is that firefox is, for some reason, locking down cross-origin requests arising from <style> tags in a way that is less permissive than either
a) its treatment of fetch requests
b) chrome's treatment of requests arising from <style> tags

[jcreedcmu]

This behavior may be considered "working as intended" from firefox's point of view:
https://bugzilla.mozilla.org/show_bug.cgi?id=1201160
https://bugzilla.mozilla.org/show_bug.cgi?id=1336364

[jcreedcmu]

An example of someone else encountering a similar issue with code-server: continuedev/continue#12135

[jcreedcmu]

I feel like I have a reasonably clear idea of what's happening now, but most solutions that are coming to mind right now are not great. For example, monkeypatching infoview to do a fetch and then add a <script> tag, which tbh confuses me that that is possible. I'm not sure I fully understand yet why firefox has chosen to erect this particular security barrier.

[Vtec234]

The infoview dynamically fetches some JS scripts whose paths are stored in its HTML here. Could it also fetch CSS that way? (Sorry if I'm misunderstanding the issue, I only gave a cursory reading.)

[jcreedcmu]

Running

document.querySelectorAll('link[rel="stylesheet"]').forEach(async link => {
  try {
    const res = await fetch(link.href);
    if (!res.ok) return;
    const css = await res.text();
    const style = document.createElement('style');
    style.textContent = css;
    link.replaceWith(style);
  } catch (e) {}
})

in the console in specifically the context of the infoview iframe does cause the hovers to work, but then the "Codicon" font doesn't load, and we get some ugly unicode fallback characters (in the private use) range that are meant to be icons rendered by the icon font. I don't yet understand why the font doesn't load; it smells like it might be a slightly different reason.

[jcreedcmu]

The infoview dynamically fetches some JS scripts whose paths are stored in its HTML here. Could it also fetch CSS that way? (Sorry if I'm misunderstanding the issue, I only gave a cursory reading.)

Fundamentally I think you're understanding correctly, and I think we can do that. (I see in the network view the .js file requests at similar urls, and they all succeed) I'm just wondering whether we have to push an upstream change up to infoview, or patch it ourselves somehow.

[Vtec234]

Does lean4web have a custom patch for this? If so, fixing upstream may be better than fixing each web-based consumer.

[jcreedcmu]

Hm, I don't know.

I was thinking it was a bit much to patch upstream for a "specifically workbench issue", but maybe the right argument is it's "an issue whenever you want to deploy the lean vscode extension in a browser-embedded vscode", and workbench is just one example of that happening, so maybe an upstream fix is appropriate.

[jcreedcmu]

The "Codicon" font also loads okay on chrome, so whatever is happening on firefox is most likely also to do with its differing security policy choices.