Michael Lindgren (Oct 31 2022 at 15:05): Michael Lindgren (Oct 31 2022 at 15:05):When I run dune coq top, is there a way to get dune to pass the flags defined in my (coq.theory ...) to coqtop, so I don't have to do it manually? I thought dune would do this, but I couldn't get it to work. For example, say I have a dune file with
(coq.theory
(name minimal)
(flags -w -notation-overridden))
and a file Test.v in the same folder with contents: Notation "a + b" := (Nat.mul a b) : nat_scope. then dune builds fine without warnings, but:
$ cat Test.v | dune coq top Test.v
Done: 100% (4/4, 0 left) (jobs: 0)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]
here I would expect not to get a warning. I'm probably misunderstanding something about setting up Coq projects in dune, or I'm misunderstanding what dune coq top is supposed to do, or I've done something else wrong, in any case it would be nice to know how to do this.
Karl Palmskog (Oct 31 2022 at 15:07):I don't think the flags are read when you do dune coq top. (flags -w -notation-overridden -w) works fine for me in batch mode (dune build).
Michael Lindgren (Oct 31 2022 at 16:07):Yes dune build does the right thing, and dune coq top sets the correct -R parameter at least.
I was hoping it would also set any other flags I specify in (flags ...) so I don't end up in interactive sessions with flags different from what I compile with.
Ali Caglayan (Oct 31 2022 at 17:16):@Michael Lindgren That's surely a bug in dune coq top, can you open an issue in ocaml/dune? Should be easy to fix.
Ali Caglayan (Oct 31 2022 at 17:18):One workaround you could to for the moment is have a shell script that passes the correct flags to coqtop and any other flags. Something like mycoqtop.sh:
#!/bin/sh
coqtop -w -notation-overridden $@
And then dune coq top --toplevel=./mycoqtop.sh. (You might have to chmod +x mycoqtop.sh too).
Ali Caglayan (Oct 31 2022 at 17:26):One question: Are you running dune coq top in the same directory as where the dune file lives or in a parent directory?
Michael Lindgren (Oct 31 2022 at 17:28):Thanks, I'll file a bug report. Yes, I'm running dune coq top in the same directory as where I have both the dune file and the .v-file.
Michael Lindgren (Oct 31 2022 at 18:04):For reference, bug report: #6366.
@Ali Caglayan I think that workaround will fit in perfectly with the other workaround I had for convincing PG to invoke dune coq top in the correct opam switch. Which by the way was the workaround I was trying to get rid of when I stumbled on this issue. But instead I ended up with two workarounds.
Ali Caglayan (Oct 31 2022 at 19:15):I've also just noticed inspecting the code that you can pass args directly too.
$ dune coq top --toplevel=echo foo.v -- -w -notation-overridden
will pass the args after -- to coqtop.
Ali Caglayan (Oct 31 2022 at 19:15):Obviously that's not great for a list of warnings
Paolo Giarrusso (Oct 31 2022 at 20:06):@Michael Lindgren how did you get PG to invoke dune coq top, did you use a PG patch or is this now supported?
Ali Caglayan (Oct 31 2022 at 20:17):I believe it was possible with some hassle. @Rodolphe Lepigre would know. We didn't change anything on the Dune end recently.
Michael Lindgren (Oct 31 2022 at 20:37):@Paolo Giarrusso I used a shell-script inspired by this comment. But I think it was mostly pure luck that it worked.
Ali Caglayan (Nov 01 2022 at 01:25):Fixed: https://github.com/ocaml/dune/pull/6369
Rodolphe Lepigre (Nov 01 2022 at 17:40):Ali Caglayan said:
I believe it was possible with some hassle. Rodolphe Lepigre would know. We didn't change anything on the Dune end recently.
Actually, I don't! :) I really am hopeless at emacs/PG configuration, so the solution that @MackieLoeffel proposed in the comment pointed at by @Michael Lindgren is the best option I am aware of.
Ideally, someone will extend PG to detect a dune workspace, but that person is definitely not me.
Emilio Jesús Gallego Arias (Nov 02 2022 at 14:32):Rodolphe Lepigre said:
Ideally, someone will extend PG to detect a dune workspace, but that person is definitely not me.
I'm not sure what Tuareg / merlin uses in emacs, but actually that's not so tricky, in the sense that you can just use locate-dominating-file for dune-project
Emilio Jesús Gallego Arias (Nov 02 2022 at 14:33):so indeed you can have something setting coq-prog-name depending on that
Emilio Jesús Gallego Arias (Nov 02 2022 at 19:25):Ali Caglayan said:
Thanks @Ali Caglayan , can you separate the fix from the refactoring so I can review it?
Ali Caglayan (Nov 02 2022 at 19:30):Yes sorry I should have done that separately.
Last updated: Oct 13 2024 at 01:02 UTC