LO
а разве не с этого надо начинать?
Size: a a a
2021 July 07
BK
вот насчет вот этого и развития было бы интересно взглянуть
BK
да нет, наверное с этого, просто неожиданный переход к ОЧЕНЬ прикладной теме
Это не нужно, под Emacs есть Proof General
LO
ещё и емакс!
сразу работает
AG
рогозин как-то писал обзорчик https://serokell.io/blog/formal-verification-history
но я не парился и первое время вообще работал в простом CoqIDE
там ваще всё из коробки
LO
ты не понимаешь сути изучения чего-либо в айти. сначала надо скомпилять свежий language-server под максимально всратый редактор и ОС
LO
впрочем емакс всратый
AG
вскод как раз менее всратый же :)
LO
емакс - лучший редактор в мире. жалко только тормозной
наоборот
когда я это осознал, я стал несчастлив(
когда я это осознал, я стал несчастлив(
A
понаставят себе ленгуидж серверов, а потом жалуются на тормоза
LO
никто не заставляет емакс быть таким синхронным
блять да
они ещё туда завозят libgccjit. по идее должно было стать лучше, но я это сбилдил и всё стало только хуже и ещё какие-то левые ошибки стали сыпаться
они ещё туда завозят libgccjit. по идее должно было стать лучше, но я это сбилдил и всё стало только хуже и ещё какие-то левые ошибки стали сыпаться
я пользуюсь Emacs не потому, что мне нравится Emacs
просто всё остальное ещё хуже
LO
вот и с хаскелем так