michael.norr...@data61.csiro.au wrote: > There is no nice way to do this on a per-theorem basis, though I can imagine an option to Holmake that would turn on some sort of logging like this. Can you make a feature request please?
Done. <https://github.com/HOL-Theorem-Prover/HOL/issues/464> > You do get per-theory timing information emitted at the end of each script file, and you could see this logging information in the .hollogs file corresponding to your script. I get the “.hollogs” directory with a recent git version (It was commit 48e9f5d88 if I recall correctly) but Holmake from Kananaskis-11 does not generate the “.hollogs” directory by default. I can get a file with per-theory timing information with “Holmake --logging” in Kananaskis-11, but it is created in the current directory. ramana.ku...@cl.cam.ac.uk wrote: > In case it's not obvious, the place to make feature requests is here: > https://github.com/HOL-Theorem-Prover/HOL/issues Thanks. P.S.: I wrote this message yesterday (UTC—05) but source forge rejected my message. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
