Honestly speaking, I like those abbreviated “power” tactics, such that "fs"
for FULL_SIMP_TAC, "rfs" for REV_FULL_SIMP_TAC, etc., but using all tactics
in smaller cases (e.g. strip_tac/STRIP_TAC) doesn't make much sense to me,
because it makes me harder to distinguish between the "inner" and "outer"
languages in HOL proof scripts...
--Chun
On 27 September 2017 at 07:59, Ramana Kumar <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
>
> 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, <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?
>>
>> 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" <marioxcc...@yandex.com>
>> 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
>> hol-info@lists.sourceforge.net
>> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
