Search code examples
binaryfilesagdaagda-mode

Agda how to run compiled .agdai binaries?

I am following the docs here https://agda.readthedocs.io/en/v2.6.3/getting-started/hello-world.html#id1l

I have compiled the file, there is a binary .agdai file created in the directory but how am I meant to run it? Double clicking does nothing. Nowhere in the docs does it say how to actually run it!

Solution

  • .agdai files are not binary files but interface files, they contain a cached version of the data produced by the Agda typechecker that it can use to avoid rechecking a file if it hasn't changed.

    To compile an Agda file, you need to use one of the backends (the GHC backend and JavaScript backend are included, but there are also others that you can install separately). You can find a small tutorial on how to compile an Agda program in the user manual.