Custom Query (361 matches)

This is GNU Emacs 23.x on Linux or Mac OS.

The default proof-full-annotation uses a lot of resources, both on the Emacs and ML side, resulting in odd instabilities.

For example, open the file Isabelle2011/src/HOL/Auth/Message.thy and assert the whole buffer. This is quite slow, and there is a good chance that it stops in the middle with an Interrupt from the prover (which indicates some low-memory situation).

For this reason, the distributed Proof General is patched to have proof-full-annotation disabled by default.

When I try to process the attached Coq file using ProofGeneral, it gets hung up on the Definition of IB6_IB7_QueryTags_First. In contrast, coqtop file works on this file. The file was generated by Why3's Coq driver, so maybe it's doing something that's syntactically unusual.

I'm running PG 4.1 on GNU Emacs 24.2.1. The Coq version is 8.3pl4.

I installed PhoX 0.88.100524 and tried to step through phox/square-root-2.phx, but nothing works. Looks like the prompt is not recognized...

Hendrik