Custom Query (361 matches)

When I make a new file containing the two (literal) line

Definition foo a : Type := a. Arguments foo / ...

and try to evaluate it when running Coq 8.4beta2, PG accepts the first line fine (highlights it blue), highlights the second line pink, marks it as read-only, and refuses to do anything more with Coq; it refuses to stop coq with ctrl+c, ctrl+c, it gives me the following error when I try to retract the buffer and start over:

proof-add-to-queue: Assertion failed: (eq proof-shell-busy queuemode)

and it never finishes evaluating the line (where never >= 15 seconds). Given that coqtop sits there using 0% CPU and 8 MB of RAM, and coqc errors and quits after 2s, I'm inclined to think that this is either a PG problem, or a communication problem.

To reproduce it:

set the three-pane mode to true by setting the emacs variable proof-three-window-enable to t.

be sure to have a warning message at pg start (for example by using a different version of emacs thant the one it was compiled for).

open a .v file

Effect: the .v file is not displayed, the warning buffer + the response buffer are displayed instead.

I'm not sure whether this is a bug in Coq, or in Proof General.

Given the following file*:

Require Import Program Omega Bool.

Lemma bar : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma baz : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma qux : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma foo : forall x : Type, x = x.
  auto.
Qed.
Print foo.
Print foo.

Tell Coq to evaluate the entire thing, then, after it evaluates the [Require Import], tell it to not evaluate [foo] (ctrl + c, ctrl + enter on the [Lemma foo] line), then quickly change [Type] to [nat] before it finishes the proof of [qux], and then tell it to evaluate down to [Print foo], again. When I [Print foo], it shows the original definition (with [Type]), rather than the new definition (with [nat]).

*This will only work on a sufficiently slow computer with a sufficiently fast person. You may need to add more filler theorems, or increase the size of the numbers, so that it slows down enough to change the word before it gets there. I'm doing this in emacs (GNU Emacs 23.1.50.1 (i386-mingw-nt6.1.7601) of 2009-11-03 on LENNART-69DE564 (patched)) running Proof General (Version 4.1), and I have an HP running Windows 7 x64 with 4 GB of RAM and an AMD Turion(tm) X2 Ultra Dual-Core Mobile ZM-87 2.40 GHz.