What is the best thing to do if you've inadvertently published a package which conflicts with another, where the conflict involves competing definitions of an environment?
In this case, both prooftrees and bussproofs define a prooftree environment. Hence, the packages cannot be loaded in the same document without modification.
The suggested solution at LaTeX for Logicians is to rename prooftrees.sty as tableaux.sty and then find-and-replace all occurrences of prooftrees by tableaux and all occurrences of prooftress by tableau. The tableau environment can then be used for prooftrees trees and prooftree for bussproofs trees.
However, I'm not convinced this is good advice. First, tableaux.sty will not get updated when prooftrees.sty does, so it makes maintenance tricky. Second, it will no doubt generate questions from users who will eventually forget that their tableaux.sty is really a (possibly outdated) copy of prooftrees.sty.
The user who reported the conflict suggested I rename prooftrees as tableaux and prooftree as tableau. But the existence of the tableaux package ruled out this name in the first place.
However, it does turn out that tableaux actually includes tableau.sty and not tableaux.sty, as I'd been assuming.
One way to workaround the issue at the document level is to add something like
\usepackage{prooftrees}
\let\othername\prooftree
\undef\prooftree
\undef\endprooftree
\usepackage{bussproofs}
to the preamble of the document. othername can then be used for prooftrees trees and prooftree for bussproofs trees.
One thing I could do, therefore, would be to include a tableaux.sty in prooftrees which loads prooftrees.sty and then does
\usepackage{prooftrees}
\let\tableau\prooftree
\undef\prooftree
\undef\endprooftree
so that users who say
\usepackage{tableaux}
\usepackage{bussproofs}
can use tableau for prooftrees trees and prooftree for bussproofs trees.
This has obvious disadvantages: tableaux.sty will be provided by prooftrees rather than tableaux, while tableau.sty is provided by tableaux. Moreover, the tableau environment will also be provided by prooftrees rather than tableaux. However, I don't think this would produce a conflict with tableaux because tableau.sty provides neither tableau nor tableaux, as far as I can tell, and neither does minimum.sty, the other package file included in tableaux.
But the approach would also require users to load the packages in the correct order, as it won't work if people write
\usepackage{bussproofs}
\usepackage{tableaux}
Or I could make tableaux.sty the main file and have prooftrees.sty load tableaux.sty and then
\let\prooftree\tableau
\undef\tableau
\undef\endtableau
Or I could test at the end of the preamble whether prooftree is defined and make it an alias for tableau, if not.
But all of these options are messy and complicated. Moreover, I'm not sure if the above workaround is really safe or not.
In chat, barbara suggested just adding a workaround into the documentation. However, I wonder how many people will actually read that rather than turning to the net and creating a personalised tableaux.sty. On the other hand, maybe I am overstating the disadvantages of people doing this and this isn't such a bad workaround after all.
Of course, it would all be a lot easier if bussproofs defined bussproof rather than prooftree .... :(
