Stream: Coq Platform devs & users

Topic: Windows escaping

Enrico Tassi (May 04 2021 at 13:21):

I need some help with https://github.com/coq/coq/pull/14217/ , I need a way to pass a bucnh of arguments "arg number 1" "arg = two" to a bat file via call... Is there a way?

Enrico Tassi (May 04 2021 at 13:23):

The current code makes the argument being chopped at the :, so this is the leftover after -override-dev-pkg=coqide=https: is considered as the first argument:

//gitlab.com/coq/coq#dce3ebc791fa19f414bc6f2f7d36088760f76097 -override-dev-pkg=coqide=https://gitlab.com/coq/coq#dce3ebc791fa19f414bc6f2f7d36088760f76097

Enrico Tassi (May 04 2021 at 13:24):

Context: I need to override the URL of coq/coqide .dev packages with one pointing to the precise commit of a PR. On the platform side I think I have the right code to parse and create on the fly an overlay package. But I'm getting crazy passing arguments down to .bat files.

Gaëtan Gilbert (May 04 2021 at 13:42):

why do it in the yml instead of doing it in the .bat?

Enrico Tassi (May 04 2021 at 13:43):

that may work, let me try

Enrico Tassi (May 04 2021 at 13:45):

Illegal parameter -override-dev-pkg=coq=${CI_PROJECT_URL}#${CI_COMMIT_SHA}

Enrico Tassi (May 04 2021 at 13:45):

hum, my mistake

Enrico Tassi (May 04 2021 at 13:47):

ok, now expansion happens, and I get the same problem

Enrico Tassi (May 04 2021 at 13:48):

it may also be on the platform PR, but I don't think so (FR: https://github.com/coq/platform/pull/103)

Enrico Tassi (May 04 2021 at 13:50):

it seems call foo.bat "-a=b:c" is actually passing to foo.bat 2 arguments, -a=b and c.

Gaëtan Gilbert (May 04 2021 at 14:05):

I don't understand this log https://gitlab.com/coq/coq/-/jobs/1234908347
it says

Install cygwin and download, compile and install OCaml and Coq for MinGW
//gitlab.com/coq/coq#6558e3080567d15951dfb02f1baa616ecfba8c0b
Usage: coq_platform_make_windows [options]

the first line looks like https://github.com/coq/platform/blob/23c6b423e0a527d95768ae33646960b99f835c69/coq_platform_make_windows.bat#L220
but then why does it not echo "!!! Illegal parameter" after?

Enrico Tassi (May 04 2021 at 14:06):

ahhaha my last attempt worked

Enrico Tassi (May 04 2021 at 14:06):

it makes no sense ;-)

Michael Soegtrop (May 04 2021 at 14:36):

@Enrico Tassi : a few important points:

• if you pass a=b to CMD (afair) you get two arguments, a and b.
• if you have a single Unix EOL in a batch file, things get arbitrary, especially calls and gotos, but it still works 99.5% - the location of the failure and the LF EOL are unrelated
• windows programs do command line parsing themselves - not the shell. They get essentially a string. This is also true for CMD. If you call a batch file from cgwin, you get two command line interpretations - one by the calling bash and one by bat. E.g. if you quote something, the quotes are likely removed by bash and CMD won't see them. Low level Windows functions do support multiple separate arguments, so bash might use that, but what CMD does then is hard to know without having the sources.
• If you call a batch file from CMD, things are a bit more complicated - especially the handling of batch escapes (^ sequences) but I don't remember the details
• It might be easier to use batch escapes (^ sequences) because they don't interfere with bash

If it still doesn't make sense please let me know ;-)

Enrico Tassi (May 04 2021 at 18:00):

@Michael Soegtrop we managed to fix this, and the PR on the Coq side works. But it needs this change on the platform script https://github.com/coq/platform/pull/103 , or something equivalent. Can you give a look at it?

Last updated: Jun 03 2023 at 03:01 UTC