add entry to Makefile for generating a real Everything.agda file

[williamdemeo]

This was issue was raised before and dismissed in favor of a script. However, there have been two recent cases in which we simply forgot to import .lagda files that were meant to be imported.

We should have a standard Everything.agda file that imports (and typechecks) all modules, and we should rename our current Everything.agda to CardanoLedger.agda or something similar.

Calling what we have now Everything.agda is misleading and will confuse any outsider who decides to browse our repo; they will naturally assume the Everything.agda file imports everything (like every other Everything.agda file does).

[WhatisRT]

So there are two separate issues here:

• the workflow
• the name of the 'everything' file.

I don't really care about the second, but I don't think it's misleading. It imports everything transitively, which I think is good enough.

For the first, the setup we have now works exactly as intended. The workflow is: if you add a new module that does something completely new you need to manually add it to the top-level module. This is what the script we have enforces. If the action fails because of this, it's not a problem - it's just a reminder that you need to add this file.

Your proposal seems to be to change the workflow, so that every module in this repository is always being type checked - no more manual intervention necessary when you add something at the top. This is convenient, but has the following downsides to our current approach:

• The top-level module would basically just become a directory listing. Right now there is a bit of noise in it, but it's a relatively compact overview of all the different projects in the repository. The noise on this would be turned up to eleven.
• The git history on the top-level module would become fairly useless. Every time a module is renamed it would show up in the history of this file. You can make the argument that it shouldn't be checked in then (as the stdlib does I think), but then you just have even more loss of information. Right now, it's super easy to see when something was added, or see in a PR when a module is being added that isn't imported somewhere else. We'd lose all of this.
• This is basically a continuation of the previous point, but we'd also lose the ability to see whether e.g. a refactoring 'orphans' a module. Right now, you get an error from CI, which means you can for example delete the module if it's not being used anymore. In your proposed workflow you wouldn't see this, and we might accumulate orphan modules over time.

Overall, we'd get all of these downsides, for the upside of someone not having to write a single import once every 6 months or so. That's just not worth it.

If you thank an auto-generated everything file is useful, I don't mind adding that. But it shouldn't be what's being used by CI to ensure everything is actually being type checked. And it probably shouldn't be checked into the repository, but I wouldn't mind too much.