use lia instead of omega

Mostly to provide feedback for https://github.com/coq/coq/issues/7872, but also because with this we use lia consistently everywhere. I did the same in Iris already, the speedup was negligible though.

omega is generally faster than lia.

A bit of history: When std++ was still part of my C formalization (i.e. a long time ago), it consistently used lia at some point. But I then noticed that stuff became much faster when using omega instead. The number of uses of omega/lia in that development was probably much higher, and the it was a couple of Coq versions ago, so I don't know whether this still applies in any way.

Hmm, reading the Coq MR:

Well yeah Robbert told me about that [= lia is faster than omega] when he re-wrote Iris 3 or 4 years ago.

Now I am confused ;) Can we do some measurements comparing omega and lia on Iris/std++.

omega is generally faster than lia.

Wait, what? IIRC I learned from you that lia is generally faster than omega (and that's what I kept telling others^^). That also seems to match Joachim's experience.

On Iris, https://gitlab.mpi-sws.org/FP/iris-coq/commit/2f1ae293a543 reduced compile time by 6s or 1.2% -- that's in the noise range, I think.

I'm probably confused. From 2012:

Use [lia] instead of [omega] everywhere

https://github.com/robbertkrebbers/ch2o/commit/71c9b405487c63e79f642313e081bd7f5853ab31

So, I guess that indeed, lia is faster, and I cannot remember what I have said in the past :).

So, I guess switching to lia is indeed better. Feel free to merge.

std++ tests are still running but it seems like this PR slows things down by 0.4s or 0.5%. Again, within noise.

mentioned in commit 94359441

merged

mentioned in merge request !41 (merged)