Stream: Coq devs & plugin devs

Topic: coqc scanning PATH


view this post on Zulip Enrico Tassi (Feb 04 2022 at 14:36):

I'm trying to run the smoke-test-kit on the snap https://github.com/coq/platform/pull/211 (mostly calls to coqc) and it seems coqc snas the PATH. This in turn results in a warning, since the snap is "confined".

Any idea why coqc should scan the path? Otherwise I guess I'll have to investigate.

view this post on Zulip Gaëtan Gilbert (Feb 04 2022 at 14:38):

let require_csdp =
  if System.is_in_system_path "csdp" then lazy () else lazy (raise CsdpNotFound)

?

view this post on Zulip Guillaume Melquiond (Feb 04 2022 at 14:46):

How come the check for csdp is not inside lazy?

view this post on Zulip Gaëtan Gilbert (Feb 04 2022 at 14:51):

Enrico Tassi said:

I'm trying to run the smoke-test-kit on the snap https://github.com/coq/platform/pull/211 (mostly calls to coqc) and it seems coqc snas the PATH. This in turn results in a warning, since the snap is "confined".

Any idea why coqc should scan the path? Otherwise I guess I'll have to investigate.

if you want to be sure where it's coming from, run with -bt -w +default


Last updated: Feb 01 2023 at 14:03 UTC