Jason Gross

The documentation is correct, but the fragment you quote does not explain the difference between -Q and -R, and does not explain what happens when the fully qualified names do...

Or perhaps the documentation means the name given, and not the fully qualified name

> Read the entire paragraph (or better, all relevant parts of the `Require` doc). I don't think -Q/-R matters. I can experiment, but I'd like verify the intention. Finer details...

Yes, I rely on shadowing/hiding working in the bug minimizer

@SkySkimmer The minimizer should work now (cf https://github.com/JasonGross/coq-tools/commit/2db278b73c9f6f314f8109a0f43e6963fd16a23e); the issue was that it considered `Anomaly "in Univ.repr: Universe TList.1087 undefined."` and `Anomaly "in Univ.repr: Universe Category.Lib.TList.1086 undefined."` to be different...

> Does the minimizer need error locations to work? cc @JasonGross Generally, yes, in order to recognize the start of the error message. (Also for coqbot parsing.) The location doesn't...

Hmmm, looks like the bug minimizer hangs because the simple compiler doesn't support `-time`. Can it be given support for `-time` (and ideally `-emacs` too, which is used for locating...

I think we also need -emacs, but let's anyway try @coqbot ci minimize ci-category_theory

Urgh, probably the issue this time is that -h doesn't mention -time, or something. Let me see if I can get the minimizer to use the base version of Coq...

> Why does the minimizer need to call -h ? It uses `-h` to detect which options are supported in various versions of Coq. I guess I could just try...