I'm not going to argue about a paper written by someone whose proficiency in Coq I cannot judge with someone who doesn't seem to know anything about Coq except having read this one paper.
F* looks very good in this comparison, which is great. As you wrote above, we need better tools, and F* is getting there. Simple things can be tedious in Coq, and F* 's automation should help there.
Regarding compatibility: neither Coq nor Agda used to have much of it; nowadays Coq is maintained together with a large set of community projects, and code is much more stable. Still tons to do.
The question is not whether tactics are useful in some cases, the question how robust and stable they are, because if older libraries employing tactics no longer work, this is not a robust foundation for long-term verification efforts.
This doesn't inspire confidence, considering this author is also the most familiar with Coq of the three. He also somehow claims that Coq is stable, which I can only take to mean that it won't crash rather than that it largely preserves backwards compatibility given his difficulties. If we can't rely on some measure of backwards compatibility so we can build on stable libraries, theorem proving simple won't scale any more than programming of any kind won't scale in the same circumstances.
The number of lines of code required for the second task also doesn't inspire confidence that theorem proving with Coq will scale.
So I frankly can't see any reason to think that Coq even with tactics is a viable approach to real world verification beyond exploratory toy examples. No doubt we have different goals in mind when it comes to verification/theorem proving, which is why you think Coq is suitable and I do not.