Add test case for coq + env

[rgrinberg]

cc @ejgallego

[ejgallego]

Let's add this test and try to address the bug.

[ejgallego]

@rgrinberg I'm much afraid that after a bit of debugging I have no idea what is going on here; I can observe 3 calls to Env_node.make:

env_node_make: { dir : _build/default; scope: <anonymous .>; profile: unsound; val: [ "-type-in-type" ] }
env_node_make: { dir : _build/default; scope: <anonymous .>; profile: unsound; val: [ ":standard" ] }
env_node_make: { dir : _build/default; scope: <anonymous .>; profile: unsound; val: [ ":standard" ] }

the first one, has the right configuration for the unsound profile, but no idea where are the others coming from :(

edit: never mind, this is due to us creating a couple of default_envs in Super_context

[ejgallego]

Ok, so I think I understand the issue, tho it is a bit puzzling to me; in Env_node we have:

  let coq = inherited ~field:coq ~root:config.coq Memo.Build.return in

which actually carries a bit of a different semantics to what it was understood at beginning, in this case, if the parent environment is set, we will just discard the (env (coq ...) field if present.

This is always the case, as if the (env (coq ...)) field is absent we set it to :standard

Let me try a quick fix to see if it would make sense using a similar approach to the one used in format_config with inherited_if_absent , however there seems to be a hack in Super_context which I am not sure about:

    let inherit_from =
      if Path.Build.equal dir (Scope.root scope) then
        let format_config = Dune_project.format_config (Scope.project scope) in
        Memo.lazy_ (fun () ->
            let+ default_env = Memo.Lazy.force t.default_env in
            Env_node.set_format_config default_env format_config)
      else

[ejgallego]

Ok, found indeed the right solution, but it was subtle, see #4749