PG

PG copied to clipboard

Perhaps this is a very uncommon situation, I just installed Coq 8.6 using the Windows installer, and I also installed ProofGeneral from this repository...

The issue is that when using Coq "Compile Before Require" I get an error message similar to:

coq-auto-compile: no source file for c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vo

It seems the issue is because the path c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vo is not valid---I could not use it from the command line for instance---but it worked when I removed the backslash in c\: to make it into c:...

However, after digging around I found that this string is actually the result from calling coqdep:

C:\Users\Ismael\Documents\Proyectos\SoftwareFoundations\V1-Logical-Foundations\Work>coqdep "-Q" "c:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/" "" "c:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v"
c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.vo c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.glob c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v.beautified: c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vo
c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.vio: c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vio

Hence I'm not sure whether this is an issue with ProofGeneral, or with coqdep, or with something else... unfortunately I cannot use Compile Before Require :-(

Hi @ifigueroap! thanks for your detailed bugreport. At first sight I'd say that coqdep's output is correct. The colons that are part of Windows' drive letter must indeed be escaped to disambiguate w.r.t. the colon separator that are specific to coqdep's output format. So this should be a small bug on the PG side in the code of coq-compile-before-require.

Cc @hendriktews FYI Hendrik, we'll be very soon in the process of integrating PG/xml (ideally before end-of-February), which will require at some point to freeze master... so I suggest to postpone the bugfix of #229 for a few days ;)

Now that PG/xml has been integrated, we'll be able to look at this issue. @hendriktews would you have a little time to investigate/fix this? Otherwise I'll give a try next week-end.

I tried to find out how make supports special characters (eg. colon) in file names. All what I found says there is no support for quoting in file names. Some make versions of windows seem to have a special hack to recognize the colon following a drive letter. From that it seems that coqdep is wrong, when it quotes the drive colon.

@ifigueroap: Can you include the output that coqdep produces and that contains stuff such as "c:..." in a makefile and does make on your installation works correctly with such a makefile?

A simple fix would be to replace ":" with ":" in the output of coq-par-analyse-coq-dep-exit. But this would start to break when somebody has a literal ":" sequence in a directory that contains coq files. Does anybody know what coqdep does on directories containing backslashes, colons or spaces?

Does anybody know if emacs has a proper quote removal for strings?

@hendriktews here I'm pasting the output that I wrote in the first message:

C:\Users\Ismael\Documents\Proyectos\SoftwareFoundations\V1-Logical-Foundations\Work>coqdep "-Q" "c:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/" "" "c:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v"
c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.vo c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.glob c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v.beautified: c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vo
c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.vio: c\:/Users/Ismael/AppData/Local/Temp/ProofGeneral-coq8656BLo.v c\:/Users/Ismael/Documents/Proyectos/SoftwareFoundations/V1-Logical-Foundations/Work/Basics.vio

I made some hacks in the elisp files from PG to see what was the actual command used. The path using "C:" does not work in the Windows prompt, e.g. notepad "c\:/Users..." doesn't work, but without the trailing backslash, i. e. `notepad "C:/Users..." it does work!

Let me know if I misundertood what you were asking... I'll be happy to provide as much info as necessary.

@ifigueroap Do you solve the problem, I also have this error in win 10. any idea would be appreciated.