spec: Experimental switch from shiroa to typst html bundle export

[RobinJadoul]

This moves most of the pain of working with shiroa into something more under our control, and additionally gets significant compilation speed improvements.
Minimal required typst version becomes 0.15.0 because of this.

[github-actions]

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

---

Automated review by Kimi (Moonshot AI)

[github-actions]

Codex Code Review

• High — Bundle compilation likely fails for chips using templates. bundle.typ places every chapter in a separate document, but chip.typ queries template interaction metadata from the current document. Chapters such as CPU therefore cannot see metadata emitted by IS_BIT, IS_BYTE, etc., triggering the assertion at line 77. Make interaction counts independent of document-scoped queries or include the required metadata in every document.

• Medium — HTML equation references lose outer labels. equate-lite.typ emits label metadata only for inner labels. For an outer-labeled equation such as limbs_and_carries.typ, the replacement equation receives only <equate:revoke>, so references like @limbs:eq:decomposition become unresolved. Emit equivalent metadata/label for the only-outer case.

[RobinJadoul]

High — Bundle compilation likely fails for chips using templates.

Nope, this is fine, all things state work fine with the bundle, since it's only a single compilation emitting multiple output files.

Medium — HTML equation references lose outer labels.

The outer label is added as an inner label (but without getting an extra numbering level) because outer labels seem to not work properly in html export. The reference goes to the inner label and is as such perfectly resolved.

[erik-3milabs]

1. I believe the font is too small; I can only read comfortably at 110% zoom.
2. the color scheme is 3MI's; should be Aligned/Lambdaclass's (?)
3. sidebar:
   a. the sidebar minwidth is too small; text wraps when page is made too narrow (but not narrow enough to minimize sidebar)
   b. when sidebar is minimized, the word "Navigation" is too close to the hamburger ≡
4. lightmode/darkmode:
   a. I cannot find a manual toggle; it defaults to the browser setting; I typically prefer darkmode, but not here. 🤷
   b. in darkmode, highlighted areas (e.g. Lemma 5, sec 33.3) is barely noticable
   c. in darkmode, highlight around raw sections (e.g., tags, ranges, var types, etc.) is not noticable.
5. Re: tables:
   a. Range col of virtual overview is too small for DVRM and KECCAK
   b. the "About Ecall" section has some weird itemize misalignment issue
   c. the tag column is too crammed on 10+ assumption/constraint tables
   d. the "range" column is too crammed on ~10 constraint tables
6. Re: file organization:
   a. I'd be inclined to move the .css / .js files to a separate folder. wdyt?
   b. perhaps this is also a good moment to clean this folder up and move all section .typ files to a separate folder?

That being said: thanks for taking the time to make this happen. It's great!

[erik-3milabs]

❤️

[erik-3milabs]

Also, 👏 for the fact that this now runs on my pc without crashing ❤️

[RobinJadoul]

1. I believe the font is too small; I can only read comfortably at 110% zoom.

Looked fine to me, but I'm used to a small font on my laptop. I'll switch to 18px for now, and we'll see how that looks.

2. the color scheme is 3MI's; should be Aligned/Lambdaclass's (?)

It should be easily configurable, I just went with something working that I had access to, to avoid the ugly greys I had at first.

3. sidebar:
   a. the sidebar minwidth is too small; text wraps when page is made too narrow (but not narrow enough to minimize sidebar)

There is text wrapping, but (imo) not to an unreasonable degree. It's hard to predict the max length of any chapter and avoid any wrapping at any level at all.

   b. when sidebar is minimized, the word "Navigation" is too close to the hamburger ≡

True, I'll add a space.

4. lightmode/darkmode:
   a. I cannot find a manual toggle; it defaults to the browser setting; I typically prefer darkmode, but not here. 🤷

There is (currently) no manual toggle, as I didn't want to have to deal with the pain of figuring out how to do it cleanly and adding the js required for it. For testing purposes, there's a toggle in the devtools.

   b. in darkmode, highlighted areas (e.g. Lemma 5, sec 33.3) is barely noticable
   c. in darkmode, highlight around `raw` sections (e.g., tags, ranges, var types, etc.) is not noticable.

Both somewhat dependent on (2) atm, but I'll change them to the surface/card style of the branding, rather than the subtle band. Still not very high contrast for the code blocks, but the lemmata seem to look nice (imo) and I don't really like very-high contract code blocks any way.

5. Re: tables:
   a. Range col of virtual overview is too small for DVRM and KECCAK
   b. the "About Ecall" section has some weird itemize misalignment issue

Not really a misalignment, as it's not an itemize, but just how dl is displayed by the browser. Should be possible to style it more, but I don't entirely hate it.

   c. the tag column is too crammed on 10+ assumption/constraint tables
   d. the "range" column is too crammed on ~10 constraint tables

I'll see if I can make the "peripheral" columns take up exactly the space they need, and then we hope that the "central" column doesn't get too cramped.

6. Re: file organization:
   a. I'd be inclined to move the .css / .js files to a separate folder. wdyt?

Fair, I considered it, but didn't feel like I needed it when it was just the single style.css but since then I've also added sidenotes :)

   b. perhaps this is also a good moment to clean this folder up and move all section .typ files to a separate folder?

Perhaps, not sure of a good name yet though.

[erik-3milabs]

1. I believe the font is too small; I can only read comfortably at 110% zoom.

Looked fine to me, but I'm used to a small font on my laptop. I'll switch to 18px for now, and we'll see how that looks.

👍

2. the color scheme is 3MI's; should be Aligned/Lambdaclass's (?)

It should be easily configurable, I just went with something working that I had access to, to avoid the ugly greys I had at first.

👍

3. sidebar:
   a. the sidebar minwidth is too small; text wraps when page is made too narrow (but not narrow enough to minimize sidebar)

There is text wrapping, but (imo) not to an unreasonable degree. It's hard to predict the max length of any chapter and avoid any wrapping at any level at all.

   b. when sidebar is minimized, the word "Navigation" is too close to the hamburger ≡

True, I'll add a space.

👍

4. lightmode/darkmode:
   a. I cannot find a manual toggle; it defaults to the browser setting; I typically prefer darkmode, but not here. 🤷

There is (currently) no manual toggle, as I didn't want to have to deal with the pain of figuring out how to do it cleanly and adding the js required for it. For testing purposes, there's a toggle in the devtools.

What devtools are you referring to? I don't see it documented.
Wdyt of adding a compile flag?

   b. in darkmode, highlighted areas (e.g. Lemma 5, sec 33.3) is barely noticable
   c. in darkmode, highlight around `raw` sections (e.g., tags, ranges, var types, etc.) is not noticable.

Both somewhat dependent on (2) atm, but I'll change them to the surface/card style of the branding, rather than the subtle band. Still not very high contrast for the code blocks, but the lemmata seem to look nice (imo) and I don't really like very-high contract code blocks any way.

👍

5. Re: tables:
   a. Range col of virtual overview is too small for DVRM and KECCAK
   b. the "About Ecall" section has some weird itemize misalignment issue

Not really a misalignment, as it's not an itemize, but just how dl is displayed by the browser. Should be possible to style it more, but I don't entirely hate it.

👍

   c. the tag column is too crammed on 10+ assumption/constraint tables
   d. the "range" column is too crammed on ~10 constraint tables

I'll see if I can make the "peripheral" columns take up exactly the space they need, and then we hope that the "central" column doesn't get too cramped.

👍

6. Re: file organization:
   a. I'd be inclined to move the .css / .js files to a separate folder. wdyt?

Fair, I considered it, but didn't feel like I needed it when it was just the single style.css but since then I've also added sidenotes :)

👍

   b. perhaps this is also a good moment to clean this folder up and move all section .typ files to a separate folder?

Perhaps, not sure of a good name yet though.

👍

[RobinJadoul]

What devtools are you referring to? I don't see it documented.

Firefox, in the inspector tab:

Wdyt of adding a compile flag?

It doesn't really solve the issue once we get to making it public. I'm looking at adding a manual toggle in the most "progressive enhancement" way I can manage. That should work, but it's not done yet.