Custom Query (361 matches)

Disclaimer: I am fairly new with PG and not yet used to the terminology, so feel free to correct me when I use the wrong terms.

My setup:
Ubuntu 11.10 (64bit)
GNU Emacs 23.3.1
Coq 8.3pl1 compiled with OCaml 3.11.2

Issue: When I am stepping interactively through a coq script with either the next-command instruction or with the activated electric terminator and the terminator (i.e. the dot) happens to be the last character of that line in the script file, the editor cursor jumps to the beginning of the following line. However, what I would expect is that the cursor either remains where it is or at least that it is positioned after the terminator but on the same line.

This doesn't make a huge difference when stepping through an existing script but when one is developing a new script this behaviour can become really irritating, e.g. with the electric terminator I'd practically be forced to either write each command on a new line or constantly press the back key to reposition the cursor to where I want it.

In case that the former behaviour is intentional, a switch to change the behaviour might be useful (feel free to point me in the right direction if something like this already exists, I couldn't find it so far). Otherwise adjusting this could be considered usability enhancement.

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

I wonder if there is an issue with the treatment of the colon? Below is my report (copied from the ssreflect mailing list):

A similar problem [see the quoted message below] occurred today with ssrcoq trunk on my machine after updating to proofgeneral 4.2pre120112. Neither executables of ssreflect nor the (trunk) libraries did change.

Calling from the command line by "ssrcoq -compile" succeeds as usual. Only the emacs mode is broken.

The lemma

Lemma inord_rshift n (i : 'I_n) : inord i.+1 = rshift 1 i. by rewrite rshift1 -lift0 inord_val. Qed.

now yields in proofgeneral:

Toplevel input, characters 34-41:

Error: In environment

n : nat

i : 'I_n

The term "inord i" has type "'I_?19.+1" which should be Set, Prop or Type.

The relevant lines in the *coq* buffer:

Toplevel input, characters 34-41:

Lemma inord_rshift n (i : 'I_n) : inord i.+

Error: In environment

n : nat

i : 'I_n

The term "inord i" has type "'I_?9.+1" which should be Set, Prop or Type.

Regards, Vladimir

On 25 January 2012 10:51, Vincent Siles <vincent.siles@…> wrote:

Hi there, since lots of stuff have changed in coq-svn v8.3 recently, I decided to upgrade it this morning and recompile ssr, but I have the following error (dynamic plugin compilation):

/home/vinz/boulot/coq/v8.3/bin/coqc -q -R theories Ssreflect -R src Ssreflect theories/fintype File "/home/vinz/boulot/coq/ssreflect-svn/trunk/ssreflect/ssreflect1.3_v8.3/theories/fintype.v", line 131, characters 44-45: Error: In environment T : eqType e : seq ?15 The term "T" has type "eqType" while it is expected to have type

"pred_sort ?21".

make: * [theories/fintype.vo] Erreur 1

I'm using the svn version of Coq 8.3

[vinz@hauru ssreflect1.3_v8.3]$ $COQBIN/coqtop.byte -v The Coq Proof Assistant, version 8.3pl3 (January 2012) compiled on janv. 25 2012 11:17:29 with OCaml 3.12.1

svn info gives:

Révision : 3533 Révision de la dernière modification : 3466 Date de la dernière modification: 2011-11-21 15:14:22 +0100 (lun. 21 nov. 2011)

Do I have to backtrack to pl2 ? My goal is to use Coq 8.3 and the librairies of ssr 1.3 (I don't want to use the thoeries of the trunk since I want other people to be able to compile my files).

Any suggestions ?