Paolo Giarrusso (Jun 10 2023 at 22:09): 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) ?
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.
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.
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.
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?
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.
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.
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?
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.
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: Oct 13 2024 at 01:02 UTC