Minimizer sometimes fails to inline files

[JasonGross]

I'm going to use this thread to track undiagnosed minimization inlining failures. Once a failure is debugged, it should be edited and crossed off and linked to a separate issue about that particular failure.

[JasonGross]

• https://github.com/coq/coq/pull/16967#issuecomment-1346735566 bug.verbose.log (1).zip bug.log (2).zip

• https://github.com/coq/coq/pull/17069#issuecomment-1375318245 failure to mention that some files were not inlined? bug.log (3).zip bug.verbose.log (2).zip

[SkySkimmer]

https://github.com/coq/coq/pull/17285#issuecomment-1442584205 Minimized file:

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "coqutil.Map.Interface" "-async-proofs-tac-j" "1" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 151 lines to 13 lines, then from 18 lines to 13 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
   coqtop version runner-d7iyxycj-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at f78c2d7) (f78c2d73af34e54ff64fe829c96eb7e7fc160c90)
   Expected coqc runtime on this file: 0.121 sec *)
Require coqutil.sanity.
  Class map {key value} := mk {
    rep : Type;

    get: rep -> key -> option value;

    empty : rep;
    put : rep -> key -> value -> rep;
    remove : rep -> key -> rep;
    fold{R: Type}: (R -> key -> value -> R) -> R -> rep -> R;
  }.

The Require should be reducible to just Global Unset Universe Minimization ToSet.

Also the bot failed to mention that a file was not inlined.