Может ли Agda компилироваться быстрее в пакетном режиме?

Question

Когда я компилирую программу Agda, которая использует стандартную библиотеку, компилятор тратит много времени на вывод строк, таких как:

Skipping Relation.Binary.Consequences (/home/owen/install/lib-0.6/src/Relation/Binary/Consequences.agdai).
Skipping Relation.Binary.Indexed.Core (/home/owen/install/lib-0.6/src/Relation/Binary/Indexed/Core.agdai).
Skipping Relation.Binary (/home/owen/install/lib-0.6/src/Relation/Binary.agdai).

Я предполагаю, что причина, по которой он безопасно "пропускает" их, заключается в том, чточто они уже скомпилированы (в каталогах уже есть файлы .agdai).Но он все еще тратит много времени на их пропуск, и компиляция занимает больше минуты.

Есть ли способ избежать всей этой дополнительной работы на каждом компиляции?

Answer 1

Agda должна загрузить хотя бы некоторые из этих файлов .agdai в память, чтобы иметь возможность проверять ваш собственный код, поэтому, возможно, даже если пропустить проверку этих модулей, это все равно займет некоторое время.

Answer 2

Agda и другие подобные программные системы, такие как coq, имеют интерактивные интерфейсы, обычно через Proof General, установленную в emacs.

Модульная компиляция работает в других контекстах, потому что языки программирования имеют тенденцию полагаться на поверхностные проверки имен для внешних символов, если они вообще проверяют.Agda - это система доказательств, поэтому, если она собирается выполнять свою работу, она должна каждый раз начинать с нуля и тщательно проверять все доказательства.