non-GMP bignums

Stream: mathlib4

[Mario Carneiro]

Could someone on MacOS Arm64, Linux Arm64, or Windows please do the following test on mathlib master (or any relatively recent version):

import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
#print WeierstrassCurve.ofJ_Δ

$ lake env lean Mathlib/Test.lean | grep 615279405369003338004639155390251008
                  (Eq.refl (Int.negOfNat 615279405369003338004639155390251008))))
                  (Eq.refl 615279405369003338004639155390251008)))
              (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 615279405369003338004639155390251008)
            (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 615279405369003338004639155390251008)
              (Mathlib.Meta.NormNum.IsInt.of_raw R (Int.negOfNat 615279405369003338004639155390251008))
                (Mathlib.Meta.NormNum.IsNat.of_raw R 615279405369003338004639155390251008))

[Mario Carneiro]

I'm not sure what exactly will happen if you are on one of these affected systems, it might crash or show ***** instead of a number in those locations

[Kyle Miller]

I get no output and a nonzero exit code on MacOS Arm64.

% lake env lean Mathlib/Test.lean || echo nonzero exit code
nonzero exit code

[Mario Carneiro]

cool, that's what I thought

[Mario Carneiro]

can you also confirm that on #8506 the same test works?

[Kyle Miller]

Yep:

% lake env lean Mathlib/Test.lean | grep 615279405369003338004639155390251008
                  (Eq.refl (Int.negOfNat 615279405369003338004639155390251008))))
                  (Eq.refl 615279405369003338004639155390251008)))
              (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 615279405369003338004639155390251008)
            (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 615279405369003338004639155390251008)
              (Mathlib.Meta.NormNum.IsInt.of_raw R (Int.negOfNat 615279405369003338004639155390251008))
                (Mathlib.Meta.NormNum.IsNat.of_raw R 615279405369003338004639155390251008))

[Mario Carneiro]

Great. (The bug is that some systems use GMP bignums and others don't, and these have different in-memory (and on-disk, because oleans) representations.)

Incidentally, once #8506 is merged mathlib will actually have "architecture-dependent oleans", but they deserialized from architecture-independent .ltar files. (In principle, this could even handle much more significant architecture level deviation like 32-bit systems or big-endian architectures, although there hasn't been much demand for that.)

[Mario Carneiro]

On the subject of non-GMP bignums, we saw in this other issue that lean's implementation of bignum operations has trouble with very large numbers. Maybe we should have a non-GMP system running lean4checker, to make sure that these files aren't performing computations that are infeasible for non-GMP.