Why Coq doesn't allow a theorem with admits to end with QED in Linux and Windows?

Question

I am using Coq 8.10.0. Following proof script seems to work in Mac (ignoring warning):

Lemma plus_comm : forall (n m : nat), n + m = m + n.
Proof.
  intros.
  - admit.
Qed.

But the same proof script isn't accepted in Linux (Ubuntu) and Windows. It throws following error:

(in proof plus_comm): Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.

Any idea what's going on here?

PS: I know ideally proofs with admits should end with Admitted instead of Qed/Defined. I am trying to debug a proof script.

Answer 1

Are you sure you are using the same Coq version on macOS and on the Windows/Linux? I don't remember exactly which version introduced a change in behaviour but now the default is to disallow Qed on a proof that is incomplete.

If you still want to debug a proof and need to use Qed, I would suggest using a temporary axiom:

Axiom todo : forall {A}, A.
Tactic Notation "todo" := (exact todo).

Now you can use todo as a tactic instead of admit and it will allow you to use Qed.

Answer 2

I just figured out it's not because of the operating system. It's because of LibTactics from Software Foundations (https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html). If we have LibTactics imported in Coq proof script, that allows us to put Qed at the end of a lemma with admits.