I thought I would share the approach I have to using HolyHammer currently.
I put this in my .hol-config.sml file:
load"holyHammer";
fun hh_tac ls g =
(Thread.Thread.fork
((fn () => holyHammer.hh ls (list_mk_imp g)),
[Thread.Thread.EnableBroadcastInterrupt true]);
ALL_TAC g)
Now, if I run hh_tac[] as a tactic in the middle of a proof, it will fork a
new thread (works in PolyML only) to search for a proof of the current
goal. Meanwhile I can keep working on trying to prove it manually. But if
eventually HolyHammer comes back with a proof, it will print out the call
to metis that I could have used at the point I called hh_tac.
You can pass more theorems in the list to hh_tac as context for HolyHammer
to use (which may not be visible to its database, e.g., if they are not yet
saved theorems).
If you try this and run into issues, I encourage you to reply to this email
and/or open some issues on the issue tracker.
Cheers,
Ramana
------------------------------------------------------------------------------
The Command Line: Reinvented for Modern Developers
Did the resurgence of CLI tooling catch you by surprise?
Reconnect with the command line and become more productive.
Learn the new .NET and ASP.NET CLI. Get your free copy!
http://sdm.link/telerik
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
