The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

I am sorry for my previous message. Actually I use the cvs version
of PG of some time ago and it works. I hope PG did not change much  
since.

Here is what Pierre advised me to do :


- take coq V8.1

- get w cvs version of pg :

cvs -d 
:pserver:anon AT cvs.inf.ed.ac.uk:/disk/cvs/proofgen
 login
  ---> mdp: anon
cvs -d :pserver:anon AT cvs.inf.ed.ac.uk:/disk/cvs/proofgen checkout  
ProofGeneral

 - put in you .emacs:

(setq coq-utf-safe t)

I did not re-check since I did the cvs checkout.

Good luck,


B

Le 13 mars 07 à 14:11, Benjamin Pierce a écrit :

> I've been having trouble getting (the latest) Proof General to work  
> with Coq (8.1) on a (10.4.8 intel) Mac: everything seems to load  
> fine when I visit a .v file, but the first thing that I do that  
> requires starting Coq hangs.
>
> It appears this may be an instance of the infamous "locale bug" --  
> #1 in the PG FAQ:
>
>     http://proofgeneral.inf.ed.ac.uk/FAQ
>
> If so, then the workaround is to set my locale to something else so  
> that the bytestream coming from Coq is not interpreted by Emacs as  
> UTF-8.  But I'm not sure how to do this on a Mac, or what would be  
> a good alternative setting.
>
> If someone else has solved this problem, I'd be grateful for a  
> little recipe...
>
> Thanks,
>
>     Benjamin
>
>
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club