search

agda / cubical

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

Some Files are never checked #1054

Closed felixwellen closed 11 months ago

felixwellen commented 11 months ago

I noticed that 

Cubical/Experiments/CohomologyGroups.agda

is outdated - some imports don't exist anymore. Looking at CI logs, it seems to be never checked.

felixwellen commented 11 months ago

This one seems to not check anymore as well:

Cubical/Experiments/ZCohomologyOld/MayerVietorisUnreduced.agda
felixwellen commented 11 months ago

Ah - I get it now. There is a manually edited Everything.agda and these files and a couple of others are excluded, because the don't check anymore. Do we really want to keep these files?

mortberg commented 11 months ago

Ah - I get it now. There is a manually edited Everything.agda and these files and a couple of others are excluded, because the don't check anymore. Do we really want to keep these files?

Not sure about these particular files... What does @aljungstrom think as he wrote them?

At some point we discussed deleting the whole Experiments folder as it doesn't really make sense in a library

aljungstrom commented 11 months ago

I'm fine with this disappearing. I don't see when we'd use it and I still have it backed up on some old branches.

mortberg commented 11 months ago

I'm fine with this disappearing. I don't see when we'd use it and I still have it backed up on some old branches.

Ok, feel free to make a PR deleting old files @felixwellen

felixwellen commented 11 months ago

Ok - I will. Thanks! I will be back with a PR at some point -> closing this issue.