Coq: Recent commit broke fiat-crypto (bug in behavior of `tac; [ ... ]` with respect to goal counting)

[JasonGross]

Version

The Coq Proof Assistant, version 8.8+alpha (November 2017)
compiled on Nov 4 2017 17:32:08 with OCaml 4.02.3

$ echo | ~/.local64/coq/coq-master/bin/coqtop
Welcome to Coq jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-master,master (f281a8a88e8fc7c41cc5680db2443d9da33b47b7)

Coq < Coq <

Operating system

Linux

Description of the problem

This code works fine in Coq 8.7, but fails in Coq master. The behavior in master is obviously incorrect, as replacing ; [ | ] with . all:[ > | ] makes it go through (i.e., the refine does in fact generate only two subgoals, and Coq is confused).

Axiom flat_type : Type.
Axiom interp_flat_type : flat_type -> Type.
Inductive type := Arrow (_ _ : flat_type).
Definition interp_type (t : type)
  := interp_flat_type (match t with Arrow s d => s end)
     -> interp_flat_type (match t with Arrow s d => d end).
Axiom Expr : type -> Type.
Axiom Interp : forall {t : type}, Expr t -> interp_type t.
Axiom Wf : forall {t}, Expr t -> Prop.

Definition packaged_expr_functionP A :=
  (fun F : Expr A -> Expr A
   => forall e',
       Wf e'
       -> Wf (F e')
          /\ forall v, Interp (F e') v = Interp e' v).
Goal forall (f f0 : flat_type)
            (e : forall _ : Expr (@Arrow f f0),
                Expr (@Arrow f f0)),
    @packaged_expr_functionP (@Arrow f f0) e.
  intros.
  refine (fun e Hwf
          => (fun Hwf'
              => conj Hwf' (fun v => _)) _);
    [ | ]. (* Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *)

[JasonGross]

Bisecting gives:

c24bcae8dbc2ef82f72b3351783cbf73d3b12795 is the first bad commit
commit c24bcae8dbc2ef82f72b3351783cbf73d3b12795
Author: Hugo Herbelin [e-mail]
Date: Thu Jul 27 00:29:51 2017 +0200

Fixing one part of #5669 (unification heuristics sensitive to choice of names).

This surprising bug was caused by an Id.Set which was ordering
solutions to variable-projection problems in ascii order.

We fix it by re-considering the variables involved in the solutions
using the declaration order.

Note that in practice, this implies preferring a dependent solution
over a non-dependent one.

:040000 040000 e17e993844c23af3f7e7d30fffba00719ebcb31e cc052edf626b3537ca45ad270d508e7c66be5473 M pretyping
bisect run success

[ejgallego]

Thanks @JasonGross for identifying this issue, I guess the commit should be reverted soon. I have a question, why did Travis didn't detect the breakage here?

[JasonGross]

According to the travis log, the build for https://github.com/coq/coq/pull/924 ran "3 months ago", which is before this particular bit of code made it into fiat-crypto. Additionally, at that point in time, fiat-parsers was marked as allowed-failure, because it didn't know how to recognize 8.7+alpha as a version number. Perhaps there should be a policy of needing travis to run at most 1 week (or a couple of days) before a merge? (@maximedenes?)

[ejgallego]

Thanks @JasonGross for the details. I guess this falls pretty much down in the category of "occasional 1% benign coincidental bugs" so we shouldn't IMO worry too much about it. We cannot have a perfect CI system.

[herbelin]

@JasonGross: Minor comment while a fix arrives: change the name of Hwf' into zHwf' and it will fail also in 8.7.

[JasonGross]

@herbelin ahaha, that's terrible. So I take it your commit merely exposed whatever the underlying bug is to this case?

[herbelin]

@JasonGross: I put a fix at PR#6074. By the way, thanks for the small example. It was very helpful.