fstar-mode.el icon indicating copy to clipboard operation
fstar-mode.el copied to clipboard

fslit seems to no longer work very well

Open msprotz opened this issue 4 years ago • 6 comments

Looking at https://fstarlang.github.io/lowstar/html/LowStar.html#some-valid-low-constructs it appears that code blocks for F* are no longer rendered properly

Thanks,

Jonathan

msprotz avatar Mar 13 '20 22:03 msprotz

Do you know what changed (a sphinx update maybe?)

cpitclaudel avatar Mar 14 '20 03:03 cpitclaudel

no we pinned sphinx to the previous version -- I'm observing this with my local machine:

jonathan@absinthe:~/Code/mitls-fstar (no_hsl) $ sphinx-build --version
sphinx-build 2.4.3

and also on the CI build

jonathan@absinthe:~/Code/everest-ci (master) $ git grep sphinx
server-infra/linux/.docker/Dockerfile:#Install sphinx (for the Low* tutorial)
server-infra/linux/.docker/Dockerfile:RUN pip3 install sphinx==1.7.2 sphinx_rtd_theme

msprotz avatar Mar 16 '20 18:03 msprotz

Maybe sphinx_rtd_theme, then? Can you try pinning it to a previous release and seeing if that still happens?

cpitclaudel avatar Mar 16 '20 18:03 cpitclaudel

indeed, it looks like sphinx_rtd_theme now slaps white-space: nowrap on <code> HTML tags

any way you could skip the <code> tag? right now the structure is

<pre>
<code>stuff
over
multiple
lines but with white-space nowrap
</code>
</pre>

the <pre>, per sphinx-rtd-theme, has the right CSS styling so just getting rid of the extra <code> would likely be enough

msprotz avatar Mar 16 '20 19:03 msprotz

actually, is there any way that fslit could generate the equivalent of


.. code-block:: fstar
  <contents of the F* code here>

? I'm enjoying syntax higlighting via pygments for code-blocks I manually wrote, but the fslit-generated code blocks don't seem to be enjoying this formatting

msprotz avatar Mar 16 '20 19:03 msprotz

Sorry, I missed your messages. I'd use a custom stylesheet to work around this problem; let me know if you need help writing it.

actually, is there any way that fslit could generate the equivalent of …

Yes, definitely; the reason they are not currently highlighted is that they're intended to be highlighted in js, along with running fstar.js.

cpitclaudel avatar Jun 08 '20 19:06 cpitclaudel