Stream: Coq Platform devs & users

Topic: Windows escaping


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 04 2021 at 13:42):

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

view this post on Zulip Enrico Tassi (May 04 2021 at 13:43):

that may work, let me try

view this post on Zulip Enrico Tassi (May 04 2021 at 13:45):

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

view this post on Zulip Enrico Tassi (May 04 2021 at 13:45):

hum, my mistake

view this post on Zulip Enrico Tassi (May 04 2021 at 13:47):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (May 04 2021 at 14:06):

ahhaha my last attempt worked

view this post on Zulip Enrico Tassi (May 04 2021 at 14:06):

it makes no sense ;-)

view this post on Zulip Michael Soegtrop (May 04 2021 at 14:36):

@Enrico Tassi : a few important points:

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

view this post on Zulip 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: Jan 30 2023 at 11:03 UTC