Stream: Coq devs & plugin devs

Topic: misc/11170.sh


view this post on Zulip Ali Caglayan (May 12 2022 at 10:43):

Hi @Guillaume Melquiond, there is this test in misc which you wrote but I don't quite understand.

#!/usr/bin/env bash

set -e

export PATH=$BIN:$PATH
export OCAMLRUNPARAM=s=1

${coqc#"$BIN"} misc/aux11170.v

Isn't the bash ${string#substring} syntax supposed to remove a substring? Could you explain what the intention with this test was?

view this post on Zulip Pierre Roux (May 12 2022 at 10:45):

IIRC ${var#prefix} is standard (POSIX?) shell for remove prefix from var (if present, otherwise keep var unchanged)

view this post on Zulip Ali Caglayan (May 12 2022 at 10:53):

I already have coqc in the env, so would setting OCAMLRUNPARAM=s=1 and passing coqc instead be enough?

view this post on Zulip Guillaume Melquiond (May 12 2022 at 10:54):

I am not the original author of this code. I think it was @Gaƫtan Gilbert . I guess that the motivation for this construct was to ensure that argv[0] was the canonical name of coqc.

view this post on Zulip Ali Caglayan (May 12 2022 at 10:55):

https://github.com/coq/coq/pull/13431/files

view this post on Zulip Ali Caglayan (May 12 2022 at 10:55):

Fair enough, I will get rid of the extra fluff then.

view this post on Zulip Guillaume Melquiond (May 12 2022 at 10:55):

Sure, but I only copied an already existing testcase.


Last updated: Feb 02 2023 at 13:03 UTC