К сожалению, не то, что я знаю;самое близкое, что у вас есть, - vscoq , которое, даже если немного отстать от него, находится на дорожной карте, чтобы снова стать полностью поддерживаемым после того, как Coq может говорить на LSP.
Проблема, которую я вижу с Atom, заключается в том, что егоТеперь, когда MicroSoft приобрела GitHub, будущее кажется неопределенным, и, к примеру, ему, похоже, не хватает поддержки LSP.