Stream: Coq users

Topic: `Redirect` without suffixes, also to ignore output


view this post on Zulip Paolo Giarrusso (Jun 10 2023 at 22:09):

Redirect "/dev/null" fails with Error: System error: "/dev/null.out: Operation not permitted" — is there a better way, or does even this case need a change (like possibly https://github.com/coq/coq/pull/17724) ?

view this post on Zulip Ali Caglayan (Jun 11 2023 at 11:22):

I think that's a smart change. We want the out file to be exactly what the user wrote.

view this post on Zulip Ali Caglayan (Jun 11 2023 at 15:29):

I think the .out was a mild security consideration before. But I am not too sure how serious this is.

view this post on Zulip Ali Caglayan (Jun 11 2023 at 15:30):

If we deem it undesirable to output to an arbitrary file, I suppose we can extend Redirect to include Redirect Null or something which would point to /dev/null and an equivalent on windows.

view this post on Zulip Ali Caglayan (Jun 11 2023 at 15:31):

Another question is what is the use case for redirecting to /dev/null? Simply to silence stdout/stderr?

view this post on Zulip Ali Caglayan (Jun 11 2023 at 15:36):

Then doing that with a better output infrastructure might be the more sensible thing to do. There is much cleanup we can do on this front.

view this post on Zulip Paolo Giarrusso (Jun 11 2023 at 18:56):

yes, Redirect "/dev/null" Check (foo : bar). runs the command while hiding its output, I'm sure alternatives exist.

view this post on Zulip Paolo Giarrusso (Jun 11 2023 at 19:02):

or rather: alternatives could be designed. But I'm not sure what are the other use-cases for Redirect beyond Redirect Null?

view this post on Zulip Paolo Giarrusso (Jun 11 2023 at 19:07):

@Emilio Jesús Gallego Arias also mentioned security, and I agree Redirect gives the attacker more power than coqc, but much less than make or even dune with run rules. This seems a real problem for JsCoq (so it should disable Redirect altogether), but it seems to make no difference when you're building hostile code. VsCode plugins should refuse invoking build systems unless the project is trusted by the user.

view this post on Zulip Paolo Giarrusso (Jun 11 2023 at 19:21):

But I see more of the discussion is happening on https://github.com/coq/coq/pull/17724 — my bad.


Last updated: Jun 13 2024 at 19:02 UTC