If you use the most recent working version of HOL (get it via git), then your
Holmake processes will be multi-core on a per-theory basis (i.e., where the
theory-graph of dependencies permits it, Holmake will cause theories to build
concurrently). There is currently no support for concurrent execution within a
single session.
Michael
From: hamed nemati <hn_nemati1...@yahoo.com>
Reply-To: hamed nemati <hn_nemati1...@yahoo.com>
Date: Monday, 25 July 2016 at 03:37
To: "Norrish, Michael (Data61, Canberra City)"
<michael.norr...@data61.csiro.au>, "hol-info@lists.sourceforge.net"
<hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] EVAL(tac conv rule)
Dear Michael,
Thanks for your reply, I managed to solve the problem. As a complementary
question, I wonder if HOL4 can use more than one core for its computations.
Regards,
Hamed Nemati
On Sunday, July 24, 2016 5:39 AM, "michael.norr...@data61.csiro.au"
<michael.norr...@data61.csiro.au> wrote:
One approach would be to define constants that do the abbreviation for you.
Then you should recast the theorems/definitions that EVAL is using to also use
those new constants. I'm afraid there isn't any code already around that
automatically detects repeated sub-terms, so you'd have to write some custom
SML to get exactly the behaviour you want.
Michael
From: hamed nemati <hn_nemati1...@yahoo.com>
Reply-To: hamed nemati <hn_nemati1...@yahoo.com>
Date: Sunday, 24 July 2016 at 02:59
To: HOL-info List <hol-info@lists.sourceforge.net>
Subject: [Hol-info] EVAL(tac conv rule)
Dear All,
I would be very grateful if someone can help me with the following issue,
When I am applying (RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I
get a very huge result which has sub-terms repeat several times inside. Is
there any smarter version of EVAL(tac conv rule) which avoids expanding the
same sub-terms repeatedly by for example abbreviating them. This would decrease
evaluation time and make the evaluated term much shorter.
Regards,
Hamed Nemati
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
