search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
944 stars 81 forks source link

HTML index for CakeML theories #152

Open myreen opened 8 years ago

myreen commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 6 years ago

@mn200 any progress? :)

mn200 commented 6 years ago

No - but happy to be prodded.

xrchz commented 6 years ago

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 commented 6 years ago

Both, thanks.

xrchz commented 5 years ago

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