Custom Query (361 matches)

I’m on Mac OS 10.10.2 (Yosemite), trying to build Proof General 4.2, for Aquamacs 3.2 (based on Emacs 24.4). Running make clean; make compile EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs fails with the error cascade

In toplevel form:
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
make[1]: *** [isar/isar-unicode-tokens.elc] Error 1
make: *** [compile] Error 2

Full make output at ​https://gist.github.com/peterlefanulumsdaine/92c49ce941018b594891

I am using Proof General 4.3pre131011 with the current trunk version of Coq (pre-8.5).

With 8.4pl4, if I type period to end a tactic, my goals buffer update. If I delete the period, the goals buffer changes to what it had displayed immediately before. This is the desired behavior.

With 8.5pre, when I delete the period it clears the goals buffer, and does not display again until I press the period, making it extremely difficult to replay what changes a certain tactic made to my environment.

In, e.g., the code

Ltac f := fail.
Goal True.
  Fail f.

coqtop -emacs returns

The command has indeed failed with message:
=> In nested Ltac calls to "f", last call failed.
Error: Tactic failure.

which PG assumes means that there was an error.

In other cases, PG sees "=> Error", which it takes to mean is not an error.