MELPA Build Stability?

[Chobbes]

Hi there!

Ever since switching to installing on MELPA... I feel like I have been encountering a lot more issues with my installation! So, I guess I have a couple questions...

• Is the MELPA build pointed at the master branch?
• Is the master branch supposed to be usable by the average person who would install proof general, or is it more of an "alpha" release?
• Should MELPA be pointed at another "release" branch?

The latest thing that seems messed up to me is that I had a file with this in it:

Lemma bleh :
  forall {A : Type} (x y : A),
    x = y -> y = x.
Proof.
  intros A x y H.
  rewrite <- H.
Qed.

When I ran it and tried to retract I got this message:

Error:
Anomaly
"error with no safe_id attached: Uncaught exception Stm.Vcs_aux.Expired.."
Please report at http://coq.inria.fr/bugs/.

And I'm not sure if this is an issue I would have encountered otherwise, or if it's my fault somehow, but I have this suspicion that maybe the MELPA build is a bit too experimental?

Also for the record, I'm incredibly glad that PG is on MELPA now. That's great! I'm just not sure if it has unstable updates right now.

[pmetzger]

Have you tried running the same thing under CoqIDE and seeing if it's PG or Coq that's causing it?

[Chobbes]

This example doesn't seem to crash in CoqIDE for me. Let me install it through opam and make sure it's running the same coq, though.

[pmetzger]

Then something PG is doing is different, and it is probably not Coq's fault as such.

[Chobbes]

I'm upgrading coq, and attempting to install coqide through opam. I don't think I'm using the same Coq version right now, unfortunately.

[cpitclaudel]

Then something PG is doing is different, and it is probably not Coq's fault as such.

Anomalies are always Coq's fault :) I'd try running this example in coqtop.

[Chobbes]

Hmmm. It seems to have to do with upgrading PG from MELPA, and then running package-auto-remove. When that happens PG can't retract a buffer and gives the above error, but then after restarting emacs it's fixed.

[Blaisorblade]

Thanks @Chobbes (hi there!), I just run into very similar symptoms, and got a bit more info.

• Had working ProofGeneral in Spacemacs, installed from MELPA.
• Upgraded it (still from MELPA) to get a version with some fix (#393, FWIW).
• Run into that anomaly when retracting, multiple times, even after restarting Coq. Whenever I did look at the *coq* buffer, the failing command was always Backtrack 0 0 0 .
• Found your comment, restarted Emacs, everything worked. The Coq buffer contains no occurrence of Backtrack 0 0 0, rather Backtrack NN 0 0 (with e.g. N = 43). So the anomaly seems to complain (badly) about the initial 0 being wrong, and this is only a valid bug if hot upgrade is supposed to work (which it isn't really).

This particular anomaly has at least 11 reports (https://github.com/coq/coq/issues?utf8=%E2%9C%93&q=Stm.Vcs_aux.Expired+), but this comment says:

I recommend not caring about the anomalies, they should be eliminated as the STM/protocol roadmap gets gradually implemented.