In case it's not obvious, the place to make feature requests is here:
https://github.com/HOL-Theorem-Prover/HOL/issues
Implementation detail: I would guess you could get per-theorem timing by
setting the "default prover" to one that does timing, similar to how the
--fast option sets it to one that skips the proof.
On 27 September 2017 at 11:12, <[email protected]> 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?
>
> 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.
>
> Michael
>
> On 27/9/17, 15:39, "Mario Castelán Castro" <[email protected]> wrote:
>
> Hello.
>
> I want to know how much time each theorem takes to prove when
> processing
> a script file with Holmake. Does Holmake has an option for this? I
> tried
> “--d” already.
>
> Thanks in advance.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
>
> ------------------------------------------------------------
> ------------------
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
