Warning messages generated by cslib#165

Stream: CSLib

[Ching-Tsun Chou]

The file Cslib/Algorithms/Lean/MergeSort/MergeSort.lean added by cslib#165 is generating a lot of warning messages during lake build in the current main (commit: 2ee7c691667a90531229dd99bc17c22e1264b494). Could someone look into this? Those messages make it hard to tell if my own code is working correctly. Thanks in advance!

Also, perhaps Github PR actions can be configured to detect warning messages?

[Chris Henson]

There's an iofail option I've been meaning to add to CI, thanks for reminding me. (Not that it would have caught this, because this an issue I think due to not merging main before merging the PR, another issue I'll fix soon).

[Snir Broshi]

Chris Henson said:

(Not that it would have caught this, because this an issue I think due to not merging main before merging the PR, another issue I'll fix soon).

Are you planning on enabling GitHub's queue or BORS?

[Chris Henson]

I was going to use the merge queue since this seems easier to setup (and all I really want is for CI to run a final check before accepting the merge commit).

[Ching-Tsun Chou]

Actually those warning messages do seem to caused build failures on Github. After merging in the current main, the build of my PR cslib#216 now fails because of Cslib.Algorithms.Lean.MergeSort.MergeSort:
https://github.com/leanprover/cslib/actions/runs/20244965642/job/58122490430?pr=216

[Chris Henson]

cslib#223 fixes this. If you hit approve I can merge myself.

[Ching-Tsun Chou]

Just approved.

[Chris Henson]

Oh I thought that would meet the requirement that you can't approve your own PR, but it looks like it still needs another maintainer.

[Chris Henson]

Again sorry the the inconvenience, the PR for CI changes to prevent this are incoming.

[Ching-Tsun Chou]

I guess @Fabrizio Montesi needs to approve it.