For primitive arrays, the Coq kernel establishes the maximum length at 4194303 (2^22 - 1), which is the max length for arrays in OCaml in 32-bit systems. In 64-bit systems, the max length is 18014398509481983 (2^54 - 1).

Is there a fundamental reason to keep the 32-bit max? Our team is using primitive arrays and this maximum is limiting. Also Coq does use the 64-bit system length for primitive integers. So, we were wondering: can this be updated? Would such a pull request be welcome?

Thanks!

This topic was moved here from #Coq users > Primitive arrays max length by Karl Palmskog.

since this is a question about changing Coq (as opposed to only how it works currently), I'm moving this here

AFAIK Coq is still supporting 32 bits systems so the change is a bit more complicated than just updating the constant. Some conditional compilation wouldbe needed (you can take example on what's done for 63 bits primitive integers that are emulated on 32 bits arch). Otherwise dropping 32 bit support should be discussed.

I don't quite follow this argument. One can have a constant which represents the maximum array length and have definitions depend on this. I don't see how this is different from any other 32/64 bit code compatibility problem.

I'm not saying it's different, just that there is more involved than simply updating the constant.

You also have to make the vo format explicitly non portable. Otherwise, users could load proofs that this constant is 32 bits on a 64 bit system and derive an inconsistency.

Is the maximum array length an actual constant exposed to Coq? If it's just an "implementation limit" then it seems that one could safely have it different between 32 bit and 64 bit coq and still share .vo files

(the .vo format is already different between 32 and 64 bit, it is just done in a way where you can detect which it is and convert from one to the other during deserialization)

@Maxime Dénès : as far as I can tell from discussions the .VO format is anyway incompatible between 32 and 64 bit, but indeed one should add an explicit test. And talking of this: it would really help Coq Platform if all 64 bit formats would be compatible.

@Mario Carneiro https://github.com/coq/coq/blob/b8ba7d60e5751801b2d4fd0c551b10c6adb581d5/theories/Array/PArray.v#L39 (so actual exposed constant)

I don't think it's very hard to implement a slightly less efficient variant of persistent arrays for 32-bit architectures that can have length up to 2⁵⁴-1. We're already having non-uniform implementations per-architecture for int63 for instances.

That's probably the best solution (assuming we want to keep 32 bit support which could also be discussed).

More generally, would it make sense to eventually provide an emulation of arrays of arbitrary size, using the low-level only for compactness and efficiency, but otherwise offering the "intended" bound-free mathematical abstraction?

Last updated: Oct 13 2024 at 01:02 UTC