function-references
function-references copied to clipboard
WebAssembly
Update Soundness appendix
This extends the Soundness appendix to handle semantic types – now renamed to dynamic types.
@conrad-watt, PTAL.
One subtlety is that during reduction, we are actually dealing with a mixture of static and dynamic types:
- Type annotations in the program are static.
- But the contexts derived from module instances in frames are dynamic.
- Types looked up from the context will hence be dynamic as well.
- The types derived for admin instructions like ref.func and frame are dynamic.
This should be fine, since both typeidx and typeaddr are always expanded to functype before doing anything else to them, so it is okay for both to coexist and even get mixed.
But it means that for the soundness proof, all judgements need to be generalised to S;C context pairs, including the ones solely operating on types. So some complexity is added.
Hope I didn't miss anything.
Weird, I can't seem to reproduce or find the rendering errors you mention. The PDF build also works fine. Where exactly do you see them?
In the html render (make html in the core subdirectory, screenshots below).
It appears to display correctly when building the pdf version... the display error in the html version seems persistent when I rebuild but it's possible I have something weird going on locally.
That is weird, the HTML displays perfectly fine for me, both in Safari and Chrome. Which version of Chrome is yours?
Chrome 105, and I don't see any (obvious) errors in the console or the html source.
I've uploaded my built HTML here if you'd like to poke around. I've tried opening that source in another laptop and I get the same behaviour, so it's likely a generation issue.
If you don't see the same display error in your local HTML build, I'm happy to "lgtm" based on the pdf render after a final pass.
So, I see the rendering errors in your HTML. Diffing the sources, it seems that yours still imports MathJax 2.7.5, while mine uses MathJax 3. Moreover, the bump of maxBuffer is not inserted in your file, which very likely explains why yours bails out on larger formulas.
What's your Sphinx version? (sphinx-build --version). I suspect you need to update. I'm running on 5.1.1, CI currently uses 4.0.0.
diff _build/html/exec/modules.html ~/Desktop/conrad-html/exec/modules.html
4c4
< <html lang="en">
---
> <html xmlns="http://www.w3.org/1999/xhtml">
7,8d6
< <meta name="viewport" content="width=device-width, initial-scale=1.0" /><meta name="generator" content="Docutils 0.19: https://docutils.sourceforge.io/" />
<
10,12c8,10
< <link rel="stylesheet" type="text/css" href="../_static/pygments.css" />
< <link rel="stylesheet" type="text/css" href="../_static/alabaster.css" />
< <script data-url_root="../" id="documentation_options" src="../_static/documentation_options.js"></script>
---
> <link rel="stylesheet" href="../_static/alabaster.css" type="text/css" />
> <link rel="stylesheet" href="../_static/pygments.css" type="text/css" />
> <script id="documentation_options" data-url_root="../" src="../_static/documentation_options.js"></script>
15d12
< <script src="../_static/_sphinx_javascript_frameworks_compat.js"></script>
17,18c14,15
< <script>window.MathJax = {"tex": {"maxBuffer": 30720}}</script>
< <script defer="defer" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
---
> <script src="../_static/language_data.js"></script>
> <script async="async" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/latest.js?config=TeX-AMS-MML_HTMLorMML"></script>
...
My sphinx version is currently 2.4.3, so I'll experiment with bumping it.