Expected Behavior

dune coq top should pass the flags specified in the (coq.theory (flags ...)) to coqtop / the toplevel.

Actual Behavior

Flags specified in the dune file are ignored by dune coq top and not passed on to coqtop.

Reproduction

1. Create a dune file with contents

(coq.theory
  (name minimal)
  (flags -w -notation-overridden))

2. Create a file Test.v with contents Notation "a + b" := (Nat.mul a b) : nat_scope.

3. The arguments in the dune file is then not passed along to coqtop:

$ dune coq top --display=quiet --toplevel=echo Test.v
-topfile /tmp/minimal/_build/default/Test.v -R /tmp/minimal/_build/default minimal

for example, we get a warning here:

$ cat Test.v | dune coq top --display=quiet Test.v
Welcome to Coq 8.16.0

Coq < Toplevel input, characters 0-46:
> Notation "a + b" := (Nat.mul a b) : nat_scope.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]

Specifications

• Version of dune (output of dune --version): 3.5.0
• Version of ocaml (output of ocamlc --version): 4.14.0
• Operating system (distribution and version):

Additional information

• Link to gist with verbose output (run dune with the --verbose flag):