I am currently learning Coq from the book “software foundations”. I’ve met one problem when I did the exercise on Extraction. The CoqIDE 8.13.2 cannot execute “Extraction “impl.ml” ceval_step.” The error shows in the console is: System error: “impl.ml: Read-only file system”. I am using MacPro M1.
I tried to change the property of the folder to be readable and writable but it didn’t work. Is it a problem with mac os? It’s the first time I post questions in this forum, I hope my question is clear to you. Thank you so much for your help.