Support -Q

[RalfJung]

I am right now unsuccessfully trying to get find-bug to compile a Coq 8.5 development that needs the coq flags -Q . "". One would think that -R . "" adds more directory mappings and hence should work, too, but it does not. And it seems --arg can only be used to pass one additional argument, not three of them...

Actually, these flags are even specified in _CoqProject, it'd be best if the tool could just use that :D

[JasonGross]

Try --arg="-Q" --arg="". I'll add support for -Q and -f _CoqProject.

[RalfJung]

I managed to get it to work by changing the way the file imports other files, and then using -R. I tried --arg -Q --arg "." --arg "", but I guess it did not like the fact that -Q was meant as the argument for --arg instead of being a flag on its own. I didn't think of = ;-)

However, the script still did not properly inline modules it imported. I had to mass --no-minimize-before-inline to let it do any inlining. Not sure if that is related to the trouble with the flags.

[JasonGross]

Right, --arg possess things to coqc, but doesn't do any interpretation. I'm glad you got it to work.

Probably the issue is that the code doesn't support "" as a binding name (ends up trying to create modules with empty names). I'll see what I can do to fix this. Do you have a repository, a commit hash, and an invocation of the bug minimizer I can use to test it?

[RalfJung]

Repo: https://gitlab.mpi-sws.org/FP/iris-coq.git Commit: cbf119675813f19a631df7d9a4d77e76351ec0c0 Invocation in repository root: find-bug.py -Q . "" modures/cofe.v pproj-bug.v

I used -R instead of -Q and replaced the Require Export modures.base. by Require Export base., but above is what I would have expected to work.

There was no very visible error about inlining, maybe it scrolled by. Inlining worked once I added --no-minimize-before-inline.

[RalfJung]

I tried --arg="-Q" --arg="." --arg="", but unfortunately, it still passes -R . Top to Coq and that takes higher precedence, so then it complains that some files contains library folder.name where it was expecting Top.folder.name.

EDIT: It's not just the -R. It also rewrites some of the imports to add a Top in the beginning, which is just plain wrong since those files were not compiled with their name in Top. I tried messing with the source, but I absolutely cannot figure out what the heck it is doing with all these imports.

[JasonGross]

I don't have a working version of mathcomp/autosubst/ssr at the moment, but I've pushed changes that should fix the issues:

• find-bug.py now supports -Q . "" directly (don't use --arg for this)
• -R . Top is no longer prepended when any -Q option is passed (if you are curious, I just had to change the default value of libnames to [] from [(".", "Top")] in custom_arguments.py, and then add a bit of code to the argument parsing to put it back to [(".", "Top")] if there was no -Q and no -R.)

Can you see if it works for you now?

[RalfJung]

It is certainly getting much further now than it used to: it compiles the file, see the right error, and goes on doing stuff. Thanks a lot!

It will probably still fail because we have defined notation like

Notation "(≡{ Γ1 , Γ2 , .. , Γ3 } )" := (equivE (pair .. (Γ1, Γ2) .. Γ3))
  (only parsing, Γ1 at level 1) : C_scope.

which upsets the dot splitting thing. But that's a separate issue.