Check all agda files

[felixwellen]

No description provided.

[mortberg]

Some files should be kept IMO and some I don't know if we should throw out or not

[felixwellen]

Maybe I should add: I don't actually if all of them don't check. After a couple of them failed, I just removed everything not in Everything.agda

[mortberg]

Maybe I should add: I don't actually if all of them don't check. After a couple of them failed, I just removed everything not in Everything.agda

Ok, I think it would be better to check which check and then add them to Everything. Then we can decide whether we fix the broken ones or not

[mortberg]

Maybe I should add: I don't actually if all of them don't check. After a couple of them failed, I just removed everything not in Everything.agda

Ok, I think it would be better to check which check and then add them to Everything. Then we can decide whether we fix the broken ones or not

Ps: it would be good not to have a manually written Everything file. It's very easy to forget to add new files

[felixwellen]

Ps: it would be good not to have a manually written Everything file. It's very easy to forget to add new files

Yes, absolutely. We shouldn't have done that ;-)

[felixwellen]

Also note that we have more manually maintained Everything.agdas as the one in Experiments:

.PHONY : gen-everythings
gen-everythings:
	$(EVERYTHINGS) gen-except Core Foundations Codata Experiments

I guess the otheres might be more unlikely to lead to issues, since the stuff in those folders is likely to be used elsewhere. If there are files that don't check, I should have seen it by now.
I don't know why we are doing this though.

[mortberg]

Also note that we have more manually maintained Everything.agdas as the one in Experiments:

.PHONY : gen-everythings
gen-everythings:
	$(EVERYTHINGS) gen-except Core Foundations Codata Experiments

I guess the otheres might be more unlikely to lead to issues, since the stuff in those folders is likely to be used elsewhere. If there are files that don't check, I should have seen it by now. I don't know why we are doing this though.

I don't know either. Feel free to figure out which check and then we can decide what to do about those that don't, and eventually get rid of gen-except...

[felixwellen]

Some of the manual Everything.agda are about flags...

[felixwellen]

Core, Foundation, Codata all have Everything.agdas for some reason: They reexport a lot, or use some special flags, don't have a safe flag,...
So I'll leave that as it is and just switch the Experiments/Everything.agda to automatic.

[mortberg]

Let's see if @aljungstrom responds by tomorrow, otherwise you can merge. It seems silly to keep completely commented files though...

[felixwellen]

There are still some out-commented parts of files, but I think the situation is still a lot better than before, so I'll merge.

[felixwellen]

(...after the rebase checks out)