# Installation attempts on MacbookPro M3 Max give Segmentation fault: 11 errors

**URL:** <https://discourse.rocq-prover.org/t/installation-attempts-on-macbookpro-m3-max-give-segmentation-fault-11-errors/2299>\
**Category:** Using Rocq\
**Created:** [May 22, 2024, 3:27am UTC](https://discourse.rocq-prover.org/t/installation-attempts-on-macbookpro-m3-max-give-segmentation-fault-11-errors/2299 "2024-05-22T03:27:45Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![wdcraft](https://avatars.discourse-cdn.com/v4/letter/w/7feea3/32.png) [@wdcraft](https://discourse.rocq-prover.org/u/wdcraft)\
**Post date:** [May 22, 2024, 3:27am UTC](https://discourse.rocq-prover.org/t/installation-attempts-on-macbookpro-m3-max-give-segmentation-fault-11-errors/2299/1 "2024-05-22T03:27:45Z")

</div>

In my most recent attempt to install Coq on my MacbookPro M3 Max machine, and using the Platform installation script (running sh coq\_platform\_make.sh in my terminal window), I always get Segmentation fault 11 errors for two pieces (regardless of the options I choose while running the installation script). The errors always arise while compiling:  
(1) coq-unicoq.1.6+8.17  
(2) coq-relation-algebra.1.7.9  
with the error details provided in my terminal window (apologies for the detailed post) shown further down in my post.  
Anyone have any suggestions about why this might be happening and how to make things work?  
Thanks for any ideas!

```auto
#=== ERROR while compiling coq-unicoq.1.6+8.17 ================================#
# context 2.1.5 | macos/arm64 | ocaml-option-flambda.1 ocaml-variants.4.14.1+options | https://coq.inria.fr/opam/released#2024-05-13 05:50
# path ~/.opam/CP.2023.11.0~8.17~2023.08/.opam-switch/build/coq-unicoq.1.6+8.17
# command /usr/bin/make -j12
# exit-code 2
# env-file ~/.opam/log/coq-unicoq-56132-11b9a2.env
# output-file ~/.opam/log/coq-unicoq-56132-11b9a2.out
### output ###
# [...]
# make[1]: *** [test-suite/munifytest.vo] Segmentation fault: 11
# make[1]: *** Waiting for unfinished jobs....
# Decimal.uint =<= Decimal.uint (Reduce-Same)
# Decimal.uint =<= Decimal.uint (Reduce-Same)
# Number.uint =<= Number.uint (Reduce-Same)
# ?T =<= nat (Meta-Inst)make[1]: *** [test-suite/microtests.vo] Segmentation fault: 11
# make[1]: *** [test-suite/bug_41.vo] Segmentation fault: 11
# make[1]: *** [test-suite/bug_44.vo] Segmentation fault: 11
# make[1]: *** [test-suite/primitive.vo] Segmentation fault: 11
# make[1]: *** [test-suite/instantiate.vo] Segmentation fault: 11
# make[1]: *** [test-suite/timings.vo] Segmentation fault: 11
# make: *** [all] Error 2

#=== ERROR while compiling coq-relation-algebra.1.7.9 =========================#
# context 2.1.5 | macos/arm64 | ocaml-option-flambda.1 ocaml-variants.4.14.1+options | https://coq.inria.fr/opam/released#2024-05-13 05:50
# path ~/.opam/CP.2023.11.0~8.17~2023.08/.opam-switch/build/coq-relation-algebra.1.7.9
# command /usr/bin/make -j12
# exit-code 2
# env-file ~/.opam/log/coq-relation-algebra-56132-abc6dd.env
# output-file ~/.opam/log/coq-relation-algebra-56132-abc6dd.out
### output ###
# [...]
# COQC theories/traces.v
# COQC theories/lang.v
# COQC theories/atoms.v
# COQC theories/factors.v
# COQC theories/kat.v
# COQC theories/normalisation.v
# COQC theories/untyping.v
# COQC theories/glang.v
# COQC theories/rel.v
# make[1]: *** [theories/normalisation.vo] Segmentation fault: 11
# make[1]: *** Waiting for unfinished jobs....
# make: *** [all] Error 2

```

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [May 22, 2024, 9:35am UTC](https://discourse.rocq-prover.org/t/installation-attempts-on-macbookpro-m3-max-give-segmentation-fault-11-errors/2299/2 "2024-05-22T09:35:28Z")

</div>

Related issue:

> <https://github.com/damien-pous/relation-algebra/issues/44>
>
> There is a strange effect with latest MacOS (14.3.X and 14.4.X): coqc segfaults …when compiling \`theories/normalisation.v\`. It could also be caused by a change in XCode (still checking). It might well be that this is only reproducible with release binaries. This has been reproduced by several people.
> 
> In case you don't have a Mac at this OS version, we can do a remote session and look into this together.
> 
> A few notes:
> 
> \- it is not a stack overflow, but an access to an invalid pointer
> \- good instructions for creating a core dump on MacOS can be found \[here\](https://nasa.github.io/trick/howto\_guides/How-to-dump-core-file-on-MacOS.html) . applying the codesign command on the opam provided coqc did work for me.
> \- a core dump can be inspected on MacOS with \`lldb -c coredump\`
> \- this currently kills the MacOS CI for Coq Platform
> 
> The codeline which crashes is the \`fold\_expr l\` in
> 
> https://github.com/damien-pous/relation-algebra/blob/dbb5713ab490fdfabc87785e0f17370edce7723f/theories/normalisation.v#L86
> 
> 
> The resulting stack trace is:
> \`\`\`
> \* thread #1, stop reason = ESR\_EC\_DABORT\_EL0 (fault address: 0xfffffffffffffffd)
> \* frame #0: 0x0000000102ef6a24 coqc\`camlTyping\_\_execute\_2270 + 1052
> frame #1: 0x00000001033772bc coqc\`camlCArray\_\_fold\_left\_map\_1815 + 276
> frame #2: 0x0000000102ef7080 coqc\`camlTyping\_\_execute\_2270 + 2680
> frame #3: 0x00000001033772bc coqc\`camlCArray\_\_fold\_left\_map\_1815 + 276
> frame #4: 0x0000000102ef7080 coqc\`camlTyping\_\_execute\_2270 + 2680
> frame #5: 0x0000000102b28cd8 coqc\`camlTactics\_\_anon\_fn$5btactics$2eml$3a344$2c35$2d$2d489$5d\_63511 + 48
> frame #6: 0x0000000102c8f27c coqc\`camlRefine\_\_f\_666 + 20
> frame #7: 0x0000000102c8f080 coqc\`camlRefine\_\_anon\_fn$5brefine$2eml$3a109$2c28$2d$2d149$5d\_7897 + 24
> frame #8: 0x0000000102c8f00c coqc\`camlRefine\_\_anon\_fn$5brefine$2eml$3a108$2c27$2d$2d189$5d\_7961 + 52
> frame #9: 0x0000000102c8dd60 coqc\`camlRefine\_\_anon\_fn$5blogic\_monad$2eml$3a193$2c15$2d$2d96$5d\_54217 + 56
> frame #10: 0x000000010301de38 coqc\`camlLogic\_monad\_\_anon\_fn$5blogic\_monad$2eml$3a261$2c15$2d$2d254$5d\_1045 + 104
> frame #11: 0x000000010301de38 coqc\`camlLogic\_monad\_\_anon\_fn$5blogic\_monad$2eml$3a261$2c15$2d$2d254$5d\_1045 + 104
> frame #12: 0x000000010301b6e4 coqc\`camlLogic\_monad\_\_anon\_fn$5blogic\_monad$2eml$3a67$2c24$2d$2d45$5d\_22570 + 60
> frame #13: 0x000000010301ba18 coqc\`camlLogic\_monad\_\_anon\_fn$5blogic\_monad$2eml$3a67$2c24$2d$2d45$5d\_108 + 40
> frame #14: 0x000000010301caf8 coqc\`camlLogic\_monad\_\_run\_498 + 40
> frame #15: 0x0000000102c96220 coqc\`camlProof\_\_run\_tactic\_1412 + 248
> frame #16: 0x0000000102c988fc coqc\`camlProof\_\_solve\_2404 + 1516
> frame #17: 0x0000000102abd9c8 coqc\`camlComTactic\_\_anon\_fn$5bcomTactic$2eml$3a46$2c57$2d$2d435$5d\_1056 + 112
> frame #18: 0x0000000102abd678 coqc\`camlComTactic\_\_solve\_core\_98 + 288
> frame #19: 0x00000001029dd5c8 coqc\`camlVernacextend\_\_anon\_fn$5bvernacextend$2eml$3a151$2c22$2d$2d125$5d\_324 + 24
> frame #20: 0x0000000102aa3cdc coqc\`camlVernacinterp\_\_interp\_expr\_400 + 1300
> frame #21: 0x0000000102aa4654 coqc\`camlVernacinterp\_\_anon\_fn$5bvernacinterp$2eml$3a158$2c4$2d$2d444$5d\_832 + 620
> frame #22: 0x00000001032f3b1c coqc\`camlFlags\_\_silently\_349 + 92
> frame #23: 0x0000000102aa4cf4 coqc\`camlVernacinterp\_\_interp\_inner\_1098 + 268
> frame #24: 0x00000001026c3e3c coqc\`camlStm\_\_step\_103662 + 980
> frame #25: 0x00000001026b87a8 coqc\`camlStm\_\_define\_inner\_4277 + 1432
> frame #26: 0x00000001026c36f0 coqc\`camlStm\_\_reach\_inner\_54728 + 4264
> frame #27: 0x00000001026c7a28 coqc\`camlStm\_\_observe\_11877 + 152
> frame #28: 0x000000010268152c coqc\`camlVernac\_\_interp\_vernac\_145 + 268
> frame #29: 0x0000000102681a5c coqc\`camlVernac\_\_loop\_1785 + 964
> frame #30: 0x0000000102682410 coqc\`camlVernac\_\_load\_vernac\_520 + 384
> frame #31: 0x000000010268e150 coqc\`camlCcompile\_\_compile\_37 + 1384
> frame #32: 0x000000010268ea90 coqc\`camlCoqc\_\_coqc\_run\_68 + 304
> frame #33: 0x000000010267d348 coqc\`camlDune\_\_exe\_\_Coqc\_bin\_\_code\_begin + 688
> frame #34: 0x0000000102637294 coqc\`caml\_program + 11532
> frame #35: 0x000000010343abf4 coqc\`caml\_start\_program + 104
> frame #36: 0x0000000103415de8 coqc\`caml\_startup\_common(argv=0x0000000000000003, pooling=\<unavailable\>) at startup\_nat.c:160:9 \[opt\]
> frame #37: 0x0000000103415e5c coqc\`caml\_main \[inlined\] caml\_startup\_exn(argv=\<unavailable\>) at startup\_nat.c:167:10 \[opt\]
> frame #38: 0x0000000103415e54 coqc\`caml\_main \[inlined\] caml\_startup(argv=\<unavailable\>) at startup\_nat.c:172:15 \[opt\]
> frame #39: 0x0000000103415e54 coqc\`caml\_main(argv=\<unavailable\>) at startup\_nat.c:179:3 \[opt\]
> frame #40: 0x0000000103415ebc coqc\`main(argc=\<unavailable\>, argv=\<unavailable\>) at main.c:37:3 \[opt\]
> frame #41: 0x0000000198fba0e0 dyld\`start + 2360
> \`\`\`
> 
> @damien-pous (just in case you don't receive notifications for your projects - which happens)