This is certainly a nice idea. If you do figure out how to do it, please make
a pull request. In work that I haven’t polished or committed, I have
generalized our graph generation to target arbitrary theory hierarchies, and
this generates theory summaries of its own. If that’s all you want, I can try
to make it commit-able. (The fact that we have two flavours of theory
presentation in our help system is a wart all on its own…)
Michael
On 11/08/2016, 12:45, "Corey Richardson" <co...@octayn.net> wrote:
Greetings HOL developers,
As a HOL newbie, getting started trying to contribute to CakeML had me
looking for something like the HOL reference page[0] for its theories. I
made some failed attempts trying to hack up the documentation generation
tool in help/src-sml to support "arbitrary" sigobj-like directories. Has
anyone done this before, or have some advice on how to enable it? Is it
valuable to others?
[0]:
https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/HOLindex.html
Best,
--
cmr
+610481782084
http://octayn.net/
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
