Inlining can fail due to global side effects of `Require`

[JasonGross]

Consider this setup: In _CoqProject:

-R . Foo
A.v
B.v
C.v

In A.v:

Global Set Universe Polymorphism.

Axiom A : Set.

In B.v:

Definition B := Type.

In C.v:

Require Import Foo.A Foo.B.

Check (A : (B : B)).
(* Error:
The term "B" has type "Type" while it is expected to have type
"B" (universe inconsistency). *)

Inlining will first split up requires and imports, giving

Require Foo.A.
Require Foo.B.
Import Foo.A.
Import Foo.B.

Check (A : (B : B)).

Then it will try to inline Foo.B, which fails because it removes the error, because after Require Foo.A, Universe Polymorphism is set, and so B would be universe polymorphic, which removes the error. In this case, running the minimizer twice will resolve the issue.

---

Sometimes, running the minimizer twice is not enough. For example, consider this setup: In _CoqProject:

-R . Foo
D.v
E.v
F.v

In D.v:

Definition foo : 1 = 2 -> forall P, ~~P -> P.
Proof.
  intros.
  try tauto. (* no-op, unless Classical_Prop has been Required *)
  congruence.
Defined.

In E.v:

Require Import Coq.Logic.Classical_Prop.

Lemma npp : forall P, ~~P -> P.
Proof. tauto. Qed.

In F.v:

Require Import Foo.D Foo.E.

Definition bar := Eval unfold foo in foo.

Check (bar, npp) : Set.

Then if we run

find-bug.py F.v bug.v -f _CoqProject --no-admit-transparent --no-admit-opaque

we get a log ending with something like

Non-fatal error: Failed to validate all coq runs and preserve the error.
The new error was:
File "/tmp/tmpzrrXEA.v", line 20, characters 2-13:
Error: No such goal.


File not saved.
Fatal error: Sanity check failed.

which leaves over a file like

Require Import Coq.Init.Notations.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False := .
End LocalFalse.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Coq.Init.Notations.
Require Coq.Logic.Classical_Prop.

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Foo" "-top" "F") -*- *)
(* File reduced by coq-bug-finder from original input, then from 22 lines to 11 lines, then from 39 lines to 16 lines, then from 45 lines to 19 lines *)
(* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3
   coqtop version 8.8.0 (May 2018) *)
Definition foo : 1 = 2 -> forall P, ~~P -> P.
Proof.
  intros.
  try tauto.
  congruence.
Defined.

Lemma npp : forall P, ~~P -> P.
Proof.
tauto.
Qed.

Definition bar := Eval unfold foo in foo.

Check (bar, npp) : Set.

This is because moving the Requires up to the top is supposed to not break anything, but it does break things, because it changes the behavior of tactics.

---

I'm not sure how to go about fixing this, other than by asking the coqdevs for more fine-grained import control.