Coqdep: -I option for import paths doesn't work

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3995
From: @MSoegtropIMC
Reported version: 8.5
CC: @JasonGross, @maximedenes, @ppedrot, @pirbo, @Matafou

See also: BZ#5196

[coqbot]

Comment author: @MSoegtropIMC

Dear Coq Team

with Coq 8.5beta1 the -I option for coqdep doesn't seem to have any effect. I am using windows and call coqdep from make from a windows command prompt, not from a cygwin prompt. I tried absolute and relative paths with / and \ but whatever I do cogdep says thats it cannot find any of the imported .v files, which are not part of the standard library. I didn't check if it works with cygwin.

With coqdep from 8.4 this works as expected.

Best regards,

Michael

[coqbot]

Comment author: @pirbo

Have you notice this part of the CHANGES:

--8<-----

• Option -I now only adds directories to the ml path.
• New option -Q behaves as -I -as and -R, except that the logical path of
  any loaded file has to be fully qualified.
• Option -R no longer adds recursively to the ml path; only the root
  directory is added. (Behavior with respect to the load path is
  unchanged.)
  --8<-----

?

[coqbot]

Comment author: @MSoegtropIMC

Dear Pierre,

I also tried

cogdep -Q "" Top <myfile.v> > <myfile.v.d>

and

cogdep -Q "" <myfile.v> > <myfile.v.d>

Both didn't work. The file <myfile.v> imports only files in . The first results in Warnings about missing includes, the second results in an empty output, likely because <myfile.v> is interpreted as second argument of -Q.

Best regards,

Michael

[coqbot]

Comment author: @JasonGross

Have you tried
coqdep -Q "" "" <myfile.v> > <myfile.v.d>
or
coqdep -R "" Top <myfile.v> > <myfile.v.d>
?

[coqbot]

Comment author: @MSoegtropIMC

Dear Jason,

thanks for the hint! The following variants do work:

coqdep -Q "" "" <myfile.v> > <myfile.v.d>
coqdep -R "" "" <myfile.v> > <myfile.v.d>
coqdep -R "" "Top" <myfile.v> > <myfile.v.d>

this doesn't work:

coqdep -Q "" "Top" <myfile.v> > <myfile.v.d>

Thanks & best regards,

Michael

[coqbot]

Comment author: @MSoegtropIMC

Hmm, coqdep works now, but the only way I can get coqc running is

coqc -q -R "" "Top" <myfile.v>

When I use

coqc -q -Q "" "" <myfile.v>

or

coqc -q -R "" "" <myfile.v>

coqc (on Windows) seems to have trouble parsing the command line with "". It says it doesn't know what to do with <myfile.v>.

When I use -Q "Top" (as the makefiles generated by coqide suggest) I get errors when importing the resulting files:

Error: The file myfile.vo contains library Top.myfile and not library myfile

Best regards,

Michael

[coqbot]

Comment author: @maximedenes

*** This bug has been marked as a duplicate of bug BZ#3958 ***

[coqbot]

Comment author: @maximedenes

I was a bit too quick closing this bug, there is still the parsing of the empty string which is done incorrectly.

[coqbot]

Comment author: @ppedrot

The parsing of the empty string works for me under Linux, which suggests that this may not be related to Coq but rather to the way Windows handle the empty string as a command-line argument. How can we be sure about this?

[coqbot]

Comment author: @MSoegtropIMC

Dear Pierre,

as far as I know on Windows the command line parsing is done by the called executable, not byt the shell. That is the executable gets a string and parses it itself. E.g. the Microsoft C compiler has build options to do the command line with or without wildcard expansion.

See https://msdn.microsoft.com/en-us/library/8bch7bkk.aspx.

"Command-line arguments are handled by a routine called _setargv (or _wsetargv in the wide-character environment), which by default does not expand wildcards into separate strings in the argv string array. You can replace the normal _setargv routine with a more powerful version of _setargv that does handle wildcards by linking with the Setargv.obj file. If your program uses a wmain function, link with Wsetargv.obj."

But I am not sure what the Windows shell does with "". I think there might be some quoting going on by the shell. I will write a C program and test it with the different options.

Best regards,

Michael

[coqbot]

Comment author: @Matafou

Hello,

May I ask if someone is working on this?

I am in the process of fixing a number of other bugs in coqdep currently.

Best regards,
Pierre

[coqbot]

Comment author: @ppedrot

AFAIU, we were waiting to see if the empty-string parsing was Windows-specific. Otherwise, this bug is fixed, isn't it?

[coqbot]

Comment author: @MSoegtropIMC

Dear Pierre-Marie,

I did the following test:

===== test.c =====

#include <stdio.h>

int main( int argc, const char * argv[] )
{
int i;

for( i=0; i<argc; i++ )
{
    printf( "Arg %d = '%s'\n", i, argv[i] );
}

return 0;

}

===== Compilation in cygwin using mingw gcc =====

$ x86_64-w64-mingw32-gcc.exe test.c

===== Test from bash shell =====

$ ./a.exe 1 "" 2
Arg 0 = 'D:\bin\cygwin64test4\home\soegtrop\CoqBug3995\a.exe'
Arg 1 = '1'
Arg 2 = ''
Arg 3 = '2'

===== Test from DOS shell =====

D:> a.exe 1 "" 2
Arg 0 = 'a.exe'
Arg 1 = '1'
Arg 2 = ''
Arg 3 = '2'

===== Conclusion =====

it should work! Maybe you can repeat the test with the gcc you are using.

Best regards,

Michael

[coqbot]

Comment author: @ppedrot

I believe that this bug is fixed then.

[coqbot]

Comment author: @MSoegtropIMC

Dear Pierre-Marie,

I will check it with 8.6 git today and see if it is fixed.

Best regards,

Michael

[coqbot]

Comment author: @MSoegtropIMC

Dear Pierre-Marie,

the bug is fixed in 8.5pl3 and 8.6git (1 week old).

Best regards,

Michael