search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Move Everything.agda to src. #342

Closed anuyts closed 2 years ago

anuyts commented 2 years ago

Otherwise it does not seem to typecheck. I get the following error message:

The name of the top level module does not match the file name. The
module Everything should be defined in one of the following files:

but I think it means that Agda has detected that the file Everything.agda is almost but not quite part of a library. It does typecheck if I move it into src but also if I move it to a completely different location.

HuStmpHrrr commented 2 years ago

Everything is not supposed to be in src. stdlib's README also won't load. but indeed there should be a better solution.

JacquesCarette commented 2 years ago

Interestingly, stdlib does not check in its Everything.agda even though it exists. Maybe we should follow that? Indeed, their README doesn't typecheck, so I've opened https://github.com/agda/agda-stdlib/issues/1743 on the main repo to have a wider discussion.

anuyts commented 2 years ago

What is the reason for the statement "Everything is not supposed to be in src"?

HuStmpHrrr commented 2 years ago

because it is not useful as it just imports all files in the library. it's there just for typechecking the whole library by ci.

jamesmckinna commented 2 years ago

Indeed, stdlib does not check in Everything.agda, it is auto-generated by GenerateEverything.hs (which caught me out when I recently did the bulk renaming from Category.* to Effect.* (issue agda/agda-stdlib#1636). The status of README.agda is indeed also anomalous, but perhaps worth considering some sort of auto-generation for your Everything.agda... even though such an indirection then potentially disguises that dependency when global changes are made.

HuStmpHrrr commented 2 years ago

worth considering some sort of auto-generation for your Everything.agda.

It already is. it is generated by a bash oneliner.

jamesmckinna commented 2 years ago

oops... my ignorance :facepalm:

JacquesCarette commented 2 years ago

So it seems that we shouldn't check it in. I'll do that.

JacquesCarette commented 2 years ago

Closed by 8643687

anuyts commented 2 years ago

Then again, type-checking Everything.agda is an easy way to check if the library works with your current Agda installation.