I think I finally figured out why the PRE tags weren’t rendering in comments -- WordPress was stripping them out because they weren’t in the allowed tags list. The reason this was hard to track down is because apparently that list doesn’t apply to me (as an admin).
In any case, I’ve implemented a fix to what I’m pretty sure the issue was, so you should be able to put any code you add to the comments inside PRE tags now like the highlighted instructions say and it should actually work.
Hurray!
Success!!!