top-level README.agda (and Everything.agda)

[JacquesCarette]

Over in agda-categories we have agda/agda-categories#342 which is about Everything.agda that's in the repo but doesn't typecheck.

The situation is different in stdlib: Everything.agda is generated for the doc, but not in the repo. README.agda is, however, in. It has the same problem, in that it doesn't typecheck where it is (AFAIK).

I'm not quite sure what to do about it. But likely the same 'solution' is likely to apply to both libraries - thus this issue.

[MatthewDaggitt]

Err so my solution is to add . to the end of this line whenever I want to type-check the README directory:

agda-stdlib/standard-library.agda-lib

Line 2 in 1d0965c

include: src

I'm not sure there's a better solution available at the moment. Really we need a different field than include in the agda-lib files. Maybe we can convince @wenkokke to add one in while she's addressing agda/agda#5553?

[gallais]

Related: #827

[wenkokke]

Maybe we should split into “public” and “private”? @gallais?

[gallais]

I expect we will want to ensure that private modules do not leak into public ones.
That's quite a bit of work on top refactoring all of the config files. :D

[MatthewDaggitt]

That's true. Okay, I rescind my suggestion that we should try and convince you to do it while doing the refactoring!

[wenkokke]

I expect we will want to ensure that private modules do not leak into public ones.
That's quite a bit of work on top refactoring all of the config files. :D

Why? I just expect them to be unimportable, but if a public module in the same package chooses to reexport it, that’s fine?

[JacquesCarette]

I don't necessarily see the problem as README.agda not typechecking where it is, but being in the repo at all: it's a generated file. It's useful to generate the web site, but really shouldn't be checked in.

The README directory is a different thing, I agree. It almost feels like README should be its own library? [I wouldn't want to put it in a different repo.]

[wenkokke]

The README isn’t generated, is it? That’s Everything.agda?

[wenkokke]

I don't necessarily see the problem as README.agda not typechecking where it is, but being in the repo at all: it's a generated file. It's useful to generate the web site, but really shouldn't be checked in.

The README directory is a different thing, I agree. It almost feels like README should be its own library? [I wouldn't want to put it in a different repo.]

Having things such as README and Everything live in a separate library would be an easy solution.

[gallais]

Having things such as README and Everything live in a separate library would be an easy solution.

The annoying thing with this solution is that README.agda then needs to be moved to a subdirectory
because Agda does not like (for good reasons) having 2 .agda-lib files in the same directory.