lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard
verified publisher icon opencompl

chore: enable fail on warning

Open bollu opened this issue 1 year ago • 6 comments

This forces us to fix all warnings.

bollu avatar May 09 '24 21:05 bollu

we need to figure out what to do with sorrys

bollu avatar May 09 '24 23:05 bollu

Asked on Lean zulip about suppressing sorrys: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/suppress.20sorry.20warnings/near/437970722

bollu avatar May 10 '24 12:05 bollu

We only have two sorries left in proofs that we may not need. Should we just drop them and replace them with proofwanted? This this PR can go in.

tobiasgrosser avatar May 26 '24 19:05 tobiasgrosser

@tobiasgrosser that's a good idea, would you mind making the change?

bollu avatar May 29 '24 13:05 bollu

@tobiasgrosser that's a good idea, would you mind making the change?

I replaced the first: https://github.com/opencompl/ssa/pull/363.

Not sure what about the second one. Should we comment that one?

tobiasgrosser avatar May 31 '24 07:05 tobiasgrosser

I commented the last sorry. Let's see if that makes this PR green.

tobiasgrosser avatar Jun 07 '24 08:06 tobiasgrosser

This did not make it for months. Let's close it for now.

tobiasgrosser avatar Dec 11 '24 20:12 tobiasgrosser