Custom Query (361 matches)

In the coq subdirectory of PG, there's a file coq-autotest.el. In that file:

;; coq-autotest.el: tests of Coq Proof General (in progress). ;; You can run these by issuing "make test.coq" in PG home dir.

That target does not exist in the main directory's Makefile.

That behavior holds in PG 4.2 as well as the 4.3 preview I downloaded, 4.3pre150930.

Steps to reproduce:

1. load the following script, which contains a nonterminating command:

     theory Scratch imports Main begin
   
     lemma foo: "Suc x = Suc x" ..
   
     lemma "P (Suc x)"
     apply (simp add: foo)
   

2. Go to the simp-command that does not terminate

3. Perform the following actions: Undo, Interrupt, Undo, Next

Of course there is the usual warning message telling me about possible sync losses, but I somehow got used to things being "probably ok" :-)

using cvs version as of 2009-11-24 18:12 and GNU Emacs 23.1.1

see subject