The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Here is what I found out. Doing it through emacs "customization" or PG "customization" does not work since custom settings get overwritten by Coq. 

Instead one should use Coq > COQ PROG (ARGS) > Set Coq Prog *persistently* 

Alternatively one directly adds at the very end of a given file the following (in the case of impred. set):

(* 

*** Local Variables: ***

*** coq-prog-name: "...." ***

*** coq-prog-args: ("-emacs-U" "-impredicative-set")***

*** End: ***

 *)

If one works with several files at the same time the PG applies the arguments, it seems, which are set in the first of the files loaded. 

Vladimir.

 

On Apr 14, 2011, at 5:30 PM, Gregory Malecha wrote:

If you edited it outside of the emacs menus, then you'll probably need to close emacs and restart it (make sure that it doesn't revert your changes). There might be a way to do this without restarting emacs, but I don't know what it is.

On Thu, Apr 14, 2011 at 3:41 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hi,

I tried it and something (???) seems to reverse any changes to this variable.  I get the original line with the info:

String: -emacs-U

   State: CHANGED outside Customize; operating on it here may be unreliable.

   Arguments to be passed to `proof-prog-name' to run the proof assistant. More

while the saved one is -emacs-U -impredicative-set

Any ideas? (I tried doing it both through "Customization" and by introducing an extra line in .emacs). 

Thanks,

Vladimir. 

On Apr 14, 2011, at 11:22 AM, Gregory Malecha wrote:

You should be able to add -impredicative-set to your coq-prog-args variable. Something like:

(custom-set-variables

 '(coq-prog-args (quote ("-emacs-U" "-impredicative-set" ...)))

)

Hope this helps.

On Thu, Apr 14, 2011 at 10:56 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hello,

is there a way to turn on the "Impredicative Set" option in the interactive mode (e.g. in Proof General)?

Vladimir.

--
gregory malecha

--
gregory malecha