feat: usize for array types

[fgdorais]

Add efficient usize functions for Array, ByteArray, FloatArray.

This is part 1 of 2 since there is a need to update stage0 between the two parts. (See discussion below.)

Closes #4654

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-21 04:52:18)

[fgdorais]

It was necessary to update stage0 in order to use the usize functions.

[fgdorais]

awaiting-review

[nomeata]

I didn't expect this to need a stage0 update. Why is that so?

[fgdorais]

I didn't expect that either. It's because these are extern definitions so there is no code for them until stage0 is updated.

[nomeata]

Hmm, still somewhat strange, the the C symbol should already be there, shouldn’t it? Did you try setting prefer_native to true?

But I’m no expert here. I’m just bringing this up because PRs with stage0 updates need to be manually merged by (I think) Sebastian or Leo. If you’d split it in two PRs then more people can merge and it can go through the normal merge queue.

[fgdorais]

I'm not an expert there either. If I don't update stage0 then calls to usize look for the reference implementation instead of the extern symbol, but the reference implementation is never compiled.

Yes, I read the manual. I also made sure the commits were clean. I was thinking about splitting in two but I was hoping Sebastian would say something before I did that. Either way, there needs to be a stage0 update between the two commits.

[nomeata]

Right, this works of course! It’s just that with two PRs, the stage0 update can happen via the github bot. But not problem for me letting Sebastian merge this PR :-)

[fgdorais]

There's a bot for that! I thought Sebastian would have to do it either way...

I will split right away then!

[nomeata]

There is a bot these days. It runs automatically after a PR merge whenever it touches stage0/src/stdlib_flags.h, or anyone with commit rights can trigger it.

So you could even leave a comment in stage0/src/stdlib_flags.h of the form

// please update stage0

and it’ll happen automatically after the PR enters master (and it will nicely override this comment).

[fgdorais]

Thank you so much for your help Joachim! This PR would have stayed in limbo for a long time without your enlightening comments!