Coq with native compilation enabled cannot compile the library

[JasonGross]

Every time I build, I get errors such as

theories/Homotopy/ExactSequence.vo (real: 28.06, user: 26.58, sys: 1.23, mem: 597200 ko)
HOQC theories/Spaces/No/Addition
Fatal error: exception Stack overflow
Error: Native compiler exited with status 2

Command exited with non-zero status 1
theories/Spaces/Spheres.vo (real: 123.56, user: 117.66, sys: 5.67, mem: 2844152 ko)
make: *** [Makefile:910: theories/Spaces/Spheres.vo] Error 1
HOQC theories/Spaces/Torus/TorusEquivCircles
Fatal error: exception Stack overflow
Error: Native compiler exited with status 2

Command exited with non-zero status 1
theories/Spaces/Torus/TorusEquivCircles.vo (real: 371.11, user: 288.58, sys: 77.41, mem: 4923976 ko)
make: *** [Makefile:910: theories/Spaces/Torus/TorusEquivCircles.vo] Error 1
HOQC theories/Colimits/Colimit_Pushout_Flattening
theories/Colimits/Colimit_Pushout_Flattening.vo (real: 43.00, user: 34.00, sys: 7.96, mem: 968808 ko)
HOQC theories/Colimits/Sequential
Fatal error: exception Stack overflow
Error: Native compiler exited with status 2

Command exited with non-zero status 1
theories/Colimits/Sequential.vo (real: 114.35, user: 103.08, sys: 10.99, mem: 2181364 ko)
make: *** [Makefile:909: theories/Colimits/Sequential.vo] Error 1
HOQC theories/Homotopy/CayleyDickson
Fatal error: exception Stack overflow
Error: Native compiler exited with status 2

Command exited with non-zero status 1
theories/Homotopy/CayleyDickson.vo (real: 74.73, user: 61.76, sys: 12.81, mem: 1872412 ko)

These files are painfully slow. I expect this can be fixed by making select lemmas Qed rather than Defined.

[JasonGross]

Btw, to test this out yourself, you need to configure Coq itself with -native-compiler yes when building from source.

[JasonGross]

The current list of files like this:

• Categories/Grothendieck/ToSet/Morphisms.v (real: 4.86, user: 4.46, sys: 0.34, mem: 335276 ko)
• Colimits/Colimit_Flattening.v (real: 37.42, user: 33.22, sys: 4.11, mem: 932448 ko)
• Colimits/Colimit_Pushout.v (real: 21.50, user: 20.75, sys: 0.71, mem: 634780 ko)
• Colimits/Colimit_Sigma.v (real: 3.28, user: 2.95, sys: 0.28, mem: 318604 ko)
• Colimits/Pushout.v (real: 10.49, user: 10.04, sys: 0.40, mem: 342140 ko)
• Colimits/Sequential.v (real: 98.82, user: 79.62, sys: 19.09, mem: 2171940 ko)
• Homotopy/CayleyDickson.v (real: 66.82, user: 56.41, sys: 10.33, mem: 1870512 ko)
• Spaces/Spheres.v (real: 144.43, user: 110.28, sys: 33.99, mem: 2843996 ko)
• Spaces/Torus/TorusEquivCircles.v (real: 158.08, user: 123.70, sys: 34.14, mem: 4932220 ko)
• Spaces/TwoSphere.v (real: 6.81, user: 6.34, sys: 0.40, mem: 331804 ko)