search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Check all agda files #1058

Closed felixwellen closed 6 months ago

felixwellen commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 7 months ago

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

felixwellen commented 7 months ago

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.

felixwellen commented 6 months ago

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 commented 6 months ago

(...after the rebase checks out)