On Mon, Apr 06, 2020 at 09:29:05PM +0200, Guillaume Melquiond wrote: > Le 06/04/2020 à 20:12, Ralf Treinen a écrit : > > > I made a test > > and removed the mathjax lines, and I cannot see a difference. > > You can look at doc/html/technical.html#why3:transform-apply and see if > the math formula "\Gamma, h: f_1 \rightarrow f_2 \vdash G: f_2" is > correctly rendered.
Ah indeed, now I can see the difference. There is LateX math code, where the online manual at why3.lri.fr has rendered formulas. > > In that case I will just run an sed script that removes the lines > > when building the why3-doc-html package. BTW, I also tried switching > > it off in doc/conf.py, but that doesn't seem to have any effect. > > Right, mathjax is the default. > > If you want to change it, you need to register another math renderer in > conf.py, e.g., 'sphinx.ext.imgmath' (which, as its name almost implies, > invokes latex to produce .png files for each math formula). I just found that debian also has a mathjax package that allows one to install the library locally (as with jsquery and underscore). I'll try to make that work, that would of course be much better than generating images. Maybe someone should write a HeVeA plugin for sphinx ? Thanks for tour hints -Ralf. _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
