Remove warnings

[yforster]

No description provided.

[mattam82]

There's still a bit of an issue with check_todos https://github.com/MetaCoq/metacoq/runs/7077275174?check_suite_focus=true#step:4:7

[yforster]

Thanks! I think I fixed this now.

I'm a bit unsure yet how to include the checktodos. Ideally I'd like a 4th CI target which checks todos and fails if there are some, but does not affect the overall CI state of the PR. But I don't think GH actions allows such fine-grained notions

[yforster]

I tried something, let's see

[mattam82]

Also Set Warning does not seem to exist, only Set Warnings

[mattam82]

Yes, seems like a thorny issue this allow-failure: actions/runner#2347

[yforster]

Fixed!

I used allow-failure first, but then you have to click on the job to see that there are TODOs, which is a bit annoying. Now I'm trying to use if: always, but that's similarly annoying because CI becomes red when there are todos. So maybe go with the first variant where you have to click?

[mattam82]

Having to click is fine I think

[yforster]

One more try: I have a separate job which fails if there are todos, but the others are not aborted. This way the whole PR becomes red, but we can still inspect whether it compiles or not. I guess we never want to merge something with todo now, so maybe this is the way to go? Happy to revert to the click solution though

[yforster]

Do we like this? #722

[mattam82]

I like it as in actions/toolkit#722

[yforster]

Then you can merge this PR here