I've moved defCNF into the src directory so that it will be built when HOL is 
built and will be available if someone attempts to compile examples/dpll.sml

See commit a6b57a9.

The HolCheck example continues to build, but only under Moscow ML as it depends 
on being able to dynamically load the BDD code into the SML interpreter, 
something we don't know how to do for Poly/ML (their respective garbage 
collectors need to be aware of each other).  It is tested in 
tools/build-sequence.

You don't need HolCheck built to be able to use defCNF.

Thanks for the bug report,
Michael

On 05/07/12 01:05, Ramana Kumar wrote:
> The Tutorial mentions the structure defCNF, in particular the function
> defCNF.DEF_CNF_CONV in chapter 7 (page 123), but I don't think this structure 
> is
> built by default when one builds HOL.
> This can cause some confusion.
> I think it is available, though, in examples/HolCheck. Perhaps the Tutorial
> should mention that, and how to build it.
>
> On that note, I can't build examples/HolCheck because of this error:
>  > Error- in '/local/scratch/rk436/HOL/examples/muddy/MuddyCore.sml', line 6.
> Structure (Dynlib) has not been declared Found near open Dynlib
>
> Do I need to have Muddy or some other extra thing installed? If so, the 
> Tutorial
> should mention that as well (does it? - maybe I haven't read closely enough..)
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
>
>
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>



------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to