Prune `Setup.hs`

[lawcho]

Does Agda really need a Setup.hs file?

Reasons to migrate away from Setup.hs:

• Cabal discourages using Setup.hs
• Setup.hs prevents cross-compilation
• 1 extra file in the repo root
• 1 extra level of indirection in Agda's build
• Lack of developer documentation
  • about why Setup.hs is needed at all
  • about what should go in Setup.hs vs e.g. the .cabal file
• Tight (& un-documented) coupling with other parts of the codebase
  • e.g. with the Makefile, regarding the -quicker suffix
  • e.g. with Agda's command-line & IOTCM APIs, which it calls
• Other techniques exist for managing run-time data files (e.g. .agdai)
  • Case study: https://github.com/jgm/pandoc
    • Has run-time data files (LaTeX templates, CSS, etc.)
    • Has build-type: Simple (and no Setup.hs file)
    • Data files are checked in to the repo (under a data/)
    • Provides a CLI option for dumping the data files at run time (pandoc -D latex etc.)

[andreasabel]

The (only) job of Setup.hs is to build the .agdai files for the primitive library.

Why should cabal install build them? Because Agda might be installed into the root area (e.g. in a system-wide installation), and if the installation does not include building the .agdai files there, Agda will not function with just user privileges.

We could skip this step and provide a script instead that does the job, and instruct packagers and admins to use the script.
(Note that the script then needs to be portable to all OSs or we need several scripts to cover the relevant OSs).
Still, this is a bit less "batteries included".

[lawcho]

Some alternatives for generating the .agdai files:

Generate .agdai at release-time

• Add to data-files: field of .cabal
• Check .agdai in to repo
• Manually re-generate .agdai each release

Generate .agdai immediately after cabal build

• Tell packagers/users to run agda --dump-builtin-agdai-files DIR
• Precedent: Haskell installer for agda-mode.el

Generate .agdai at run-time

When agda encounters import Agda.Builtin.Nat:

• Dump Nat.agda to DIR/Agda/Builtin/Nat.agda
• Type-check contents of DIR/ as Agda source code

How to calculate DIR

1. Agda option --generated-modules-dir
   • or equivalent .agda-lib config
   • or equivalent env var
2. _build/generated-modules/ (if .agda-lib is present)
3. Wherever .agdai files normally go (e.g. in current working dir)

How to support the --safe flag

• Type check the contents of DIR/ without the --safe flag
  • Allows Agda.Builtin.Nat to contain postulate
  • Allows Agda.Builtin.Nat to contain {-# COMPILE ... #-}
• Suppress CoInfectiveImport errors for imports crossing the DIR/ boundary
  • Allows the user's code to --safely import Agda.Builtin.Nat

[gallais]

Suppress CoInfectiveImport errors for imports crossing the DIR/ boundary

This kind of ad-hoc overriding of safety checks seems dangerous.
I would rather the (already complex) safety checking logic did not have such special cases.

[andreasabel]

• Check .agdai in to repo

That's definitely a no. The repo is already too fat (my .git is 1.1GB).
Anyway, I not see why they should be checked in. They could be created on the fly when assembling the sdist tarball.

[UlfNorell]

I'm not seeing the benefits here. All the suggested alternatives for generating the agdai files put either more work on the developers or on the package maintainers. Your main complaint with Setup.hs seems to be lack of documentation, which I think is best addressed by adding documentation. If someone wants to cross-compile Agda, they can use the workaround suggested in the issue until it's been fixed.