HTML index for CakeML theories

[myreen]

The HOL build process produces an HTML index in HOL/help/HOLindex.html. Would it be possible to have a similar HTML file generated for the CakeML repo? @AndreasLoow suggested that such a feature might be handy for navigating the theories.

[mn200]

I generated something along these lines when I generated the dependency graphs; I think it's a pretty easy change to the existing DOT script in HOL. I'm not sure that the HTML format currently used is that great; I'm tempted to just link to ...Theory.sig files.

[myreen]

Linking to sig files is fine by me. I hope browsers can be made aware that they ought to treat these as normal text files.

[mn200]

Actually, .sig files can be embedded into HTML files easily enough, as done here.

I much prefer that to this example of the other HTML style.

[xrchz]

@mn200 any progress? :)

[mn200]

No - but happy to be prodded.

[xrchz]

not sure if you meant "to have been prodded" or "to be prodded in future" - consider this message to be covering the latter case

[mn200]

Both, thanks.

[xrchz]

Could we also get something like the HOLindex reference page with this? Then it could be added as a downloadable artefact after regression tests.