Extraction - System error

Using Coq
1

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.

2

Are you able to create a file in the same folder using, say, your favorite text editor? If you can, then it may be an issue in the Coq code and otherwise probably not. (Note I’ve never used Extraction.)

3

Yes. I can use a terminal to create files in the same folder.

4

Extraction uses temporary files, so it may fail if what plays the role of /tmp is on a read-only file system.

5

The function ceval_step would be extracted from “ImpCEvalFun.v”. And I am sure that this function is accessible from “Extraction.v”. I am not sure I understood your answers. here temporary files mean the generated compiled files like “ImpCEvalFun.v”? In fact, I am able to do this: “Extraction ceval_step”. The console shows the corresponding OCaml code. So, it could be that the Mac OS does not allow CoqIDE to create a file and write it.

6

You’re right, I just tested on MacOS with the CoqIDE package and it fails to extract. I could reproduce it also in VsCoq on MacOS. And it is not related to /tmp. Suspectingly rather that it tries to write in the Applications folder.

Apparently, the issue has been addressed on stackoverflow: you need to give an absolute path name.

Thanks for telling!

7

Will be fixed by Setting directory of a CoqIDE buffer to the directory of the file: this fixes failure of Extraction in CoqIDE released package by herbelin · Pull Request #14721 · coq/coq · GitHub.

Note that another alternative is to use Cd "some-writable-path". before calling Extraction.

8

Should we be including a note about this issue in the SF installation instructions?

9

Great! Thank you very much for your help.