After I built HOL4, I opened HOLDIR/help/HOLindex.html in my browser, and I clicked on the "Theory Graph" link. It was broken.
Then I read this: [70+0]hol4-source$ cat help/theorygraph/README This is the "help/theorygraph" directory for HOL. A theory dependency graph will be placed here when you build HOL (provided the Graphviz dot tool, cf. http://www.graphviz.org/, is available on your system). I most certainly do have graphviz & dot. So, thinking the configure and build process somehow misfired, I did [72+0]hol4-source$ find . -type f | xargs grep -w dot and [73+0]hol4-source$ find . -type f | xargs grep -w theorygraph Neither search returned with anything that seemed to actually look for the dot program let alone execute it. So, now it seems to me the README just lies, and the graph is not built, period. Am I right? -- Ian Zimmerman gpg public key: 1024D/C6FF61AD fingerprint: 66DC D68F 5C1B 4D71 2EE5 BD03 8A00 786C C6FF 61AD http://www.gravatar.com/avatar/c66875cda51109f76c6312f4d4743d1e.png Rule 420: All persons more than eight miles high to leave the court. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
