[acl2-books] Should disjoin, disjoin2, conjoin, and conjoin2 be disabled by default?

[David L. Rager]

Hi,

I think that every time I include GL, that it disables disjoin,
disjoin2, conjoin, and conjoin2. Should these be disabled by default
after building the system?

David

[Matt Kaufmann]

Thanks, David, for the offline discussion; so, I plan to leave things
as they are for those functions. The rest of this message just shares
some general thoughts I have on the topic of changing the default
enabled status of built-in functions.

I prefer to avoid changing the enabled status of an existing built-in
function when ACL2 starts up. My concerns are that any such change
could break things and also that I might get caught in the middle of
some argument that I don't much care about. It seems to me that in
general, people who use ACL2 system functions should take
responsibility for deciding for themselves whether to enable or
disable them.

That said, I acknowledge that there are times where there are
compelling reasons to make such a change. For example, I recall that
some years ago we changed ZP to be disabled by default. I also seem
to recall that this changed caused considerable churn -- in fact,
that's partly why I'm concerned about making such changes -- but
probably it was still a worthwhile change.

-- Matt
> Date: Sat, 21 Nov 2015 14:29:08 -0700
> From: "David L. Rager" <rag...@gmail.com>
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com

> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>