Because it’s not trivial to install it together with its dependencies (ATPs).
Last time I checked, bundling the ATPs may be difficult because of their licences (especially Vampire, which is the most effective one).
They also had impressive results which were comparable to those of CoqHammer. But I was very surprised by this, given that CoqHammer rely on very advanced ATPs and Tactician only imitates what humans have done while proving previous results.
I am not surprised. The current implementation of the “hammer” tactic in CoqHammer has many limitations - it is really a first try at a “hammer for Coq”. Among others, it doesn’t deal properly with “non-first-order” features of Coq, so it won’t work very well with developments that heavily depend on them (this includes boolean reflection, higher-order functions/predicates, dependently typed data structures). Also, “hammer” insists on using intuitionistic logic for proof reconstruction, which makes it more likely to fail (ultimately, classical logic should be optionally used in reconstruction, with a first-order reconstruction prover comparable in strength to Isabelle’s metis).
Another thing is that by design CoqHammer will never try induction, leaving this to the user. I think Tactician can use the induction tactic, so when evaluated on any reasonably large collection of Coq developments it will automatically prove many “trivial” inductive lemmas that CoqHammer won’t have any hope of proving (by design).
The main issues with CoqHammer and rough ideas of how to solve them are listed in the TODO.md file in CoqHammer sources. Tackling them would improve the usability substantially, but many require substantial engineering work and/or extensive experimentation, some with relatively low “research interest” to “software development time” ratio. Which is why I probably won’t solve these issues in any near future, and there currently don’t seem to be any other people seriously interested in getting their hands dirty with CoqHammer development.
It would be interesting to isolate “first-order” problems without induction and compare Tactician and CoqHammer on them. Then I think CoqHammer would unequivocally win. Though even on some “first-order” problems CoqHammer may fare worse than Tactician, for many reasons which I all believe to be purely technical and relatively easily solvable: the rough machine-learning premise preselection might not be good enough (it hasn’t been changed much from HOLyHammer to better adapt it to Coq), the translation might be suboptimal even for some first-order problems, intuitionistic proof reconstruction may fail with dependencies for a classical proof.
In the end, it is likely that these tools will be complementary and non-mutually-exclusive.
To some extent they already are. The advantage of the “Tactician” approach is that it’s not limited by the translation to first-order ATPs. And the mismatch between the logic of Coq and pure classical first-order logic seems to be greater than between classical higher-order logic of Isabelle and classical first-order logic.
It may be the case that CoqHammer will ever be very good only for a “first-order-like” fragment of CIC (that can still be substantially improved), and trying to adapt the “translation to ATPs” approach to broader fragments of CIC, while possible, might quickly reach a point where you get relatively little benefit for a lot of work. I think we’re still far from this point, though, and solving some of the issues in the TODO.md file could improve CoqHammer substantially.