add entry to Makefile for generating a more complete Everything.agda

[williamdemeo]

...invoke make Everything.agda to generate it.

[WhatisRT]

Thanks, but it's not all that clear to me why we'd want that. I think there are generally two options for building projects: building the least things possible starting from some root or building everything one can find.

With @Ali-Hill's script that we just merged, I think we have a pretty good setup for the former option, but this depends somewhat on us maintaining import lists, i.e. we won't find any unused modules if we import them without actually using them for anything. If we now add every module to an Everything module, that script will be completely blind and not find anything anymore.

A feature like that in the makefile would be great if we wanted to switch to the latter approach. We could then remove the Everything.agda file from the repo and just generate it automatically as part of the build instead.

I don't really have a reason to prefer one approach over the other right now, but we should probably have a good reason for switching if we do. I wonder if it's confusing to have a Everything file that doesn't actually contain everything. If we commit to the current approach, we could rename it into Main as in stdlib-meta.

[williamdemeo]

I see your point. However, my suggestion was to first run Alasdair's script to make sure there is no unnecessary/unused modules, before running make Everything.agda, or, if there is an Everthing.agda file present, then of course the script must ignore that file! 😆

If you decide we should be building a minimal amount of stuff, then I agree with your suggestion that we ought to use a different name for what is essentially the top, or entry-point, to the formal-ledger-specification code. I like your Main.agda suggestion, if that's what's used in stdlib-meta. Alternatively, I've seen Base.agda used often. I like Ledger.agda, but it seems to be overused already... how about formal-ledger-specifications.agda?

Here are a couple of reasons for not using Everything.agda for a minimal build.

As you point out, it's confusing, especially since I believe it's standard practice to list literally everything in Everything.agda (though I may be wrong about this).

If Everything.agda doesn't include everything, then it's less useful as a means of testing that every module in the library type-checks.

[williamdemeo]

When I first got the Everything.agda file of formal-ledger-specifications to type-check, I mistakenly believed I had verified that all modules in the repo type-checked. Of course, this was my own fault for not checking more carefully, but it may be an easy mistake to make.

Incidentally, in my agda-algebras library I have an Everything.agda file in case one wants to ensure everything in the library type-checks, but I don't intend for users of the library to start there. There's an agda-algebra.lagda file for that. I don't know if this is definitely the "right" way to do things... but it seems natural to me.

[WhatisRT]

Arguably all of this is a hack that just exists because Agda doesn't have a package manager and this is reasonably convenient. I don't think there'd be Everything files if there was a package manager.

I agree that it's confusing and I don't think you missing modules that weren't even in the diff is your mistake - we should (and do now) have automation in place.

I like renaming the Everything file, ideally to something that makes its purpose clear & doesn't name-clash with some other module that might pop up one day in the dependencies. Ledger is already overused, so how about FormalLedgerSpecsRoot.agda? We could also put a comment in it to make its purpose clear: to import all the modules that we consider entry points for the artifacts (PDFs & Haskell libraries) that we want to build from this repo.

[williamdemeo]

Got it. You don't want an Everything.agda. Closing.

[williamdemeo]

Resurrecting this issue because there have been two instances recently where we simply forgot to import .lagda files that were supposed to be imported. Using an ad hoc script to making sure we're importing (and type-checking) everything we want is clearly not working.