All geek questions in one place

Can Agda compile faster in batch mode?

When I compile an Agda program that uses a standard library, the compiler spends long lines of print, such as:

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).

I assume that the reason it safely skips is because they are already compiled (there are already .agdai files in the directories). But he still spends a lot of time skipping them, and the compilation takes more than a minute.

Is there a way to avoid any extra work on each compiler?

+4
source share
2 answers

Agda loads at least some of these .agdai files into memory in order to be able to check its own code, so it’s possible that even if you skip checking these modules, it still takes some time.

+1
source

Agda and other similar software systems, such as coq, have interactive interfaces, usually through Proof General, installed in emacs.

Modular compilation works in other contexts because programming languages ​​tend to rely on small name checks for external characters, if they do at all. Agda is a evidence system, so if it is going to do its job, it must start from scratch every time and deeply check all evidence.

0
source

Source: https://habr.com/ru/post/1401537/

More articles:


All Articles