On 14/11/12 08:11, F.Lockwood Morris wrote: >> That language sounds a deal more forbidding than I’d like. Can you point >> me to it so it can be fixed/removed? In any case, I’d be quite happy to >> take delivery of source code in whatever form you like.
> I'm embarrassed, I have mislaid where it was I stumbled across that, which > was probably less forbidding than I made it sound. I think a distinction was > drawn between libraries and less-overseen things called "contributions". I suppose the way we handle things now is that the distinction is between what goes into HOLDIR/src and what goes into HOLDIR/examples. The distinction is based on the degree to which we expect something to be widely used. Your work is clearly similar to the patricia tree theories, so, like that work, it should almost certainly fall into src. > Yes indeed, I intend to try that out. (And see the remainder of my reply to > Ramana.) I will send you a copy of the "Notes" (which ought to fission into a > paper and a user manual - at the moment they are just everything I could > think of to write down) when I send them to him, and my HOL files too if you > want to see them, though I don't feel they're in shape yet to speak of > "delivering" them. Certainly, I’d be interested in seeing the notes. > Once I have had Kanasaskis-8 installed here, I will appeal to you for help in > connecting to your wellorderTheory. If you did want that link, and we put your code into src, then wellorderTheory would need to go into src as well, so that linking to it would be as simple as typing open wellorderTheory just as you refer to other standard theories from src (num, real, relation, bool etc). Otherwise, you’d need to explicitly put the $(HOLDIR)/examples/set-theory/hol_sets into an INCLUDES specification in a Holmakefile. Best, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
