The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
I give you the reasons, I don't argue for them. It can be discussed.

On 22/04/2013 09:14, Gert Smolka wrote:
> At Saarland University we are teaching Coq in the Intro to Computational 
> Logic course.  Since most student don't know Emacs at this point we 
> recommend CoqIDE.  When I checked out CoqIDE on MacOs for the first lecture 
> I was surprised to get the warning
>
>    Warning: query commands should not be inserted in scripts
>
> for commands like Check, Print, and Compute.
This warning has been made a long time ago as an advertisement for
coqide feature :-) It says : "Hey developer, I've created a query pane
where you can write queries and keep the result displayed as long as you
need. Don't pollute your script with that."
or "a query is not made to remain in a proof script, if you want to
write Print foo, just select foo and press F4".
You're wright, this assertion is false for pedagogy. Personnally, I'm
happy to ignore the warning but if you are disturb by it, I think it can
be suppressed.
>   Even worse, the command "Set Printing All" is rejected and I get
>
>    Error: Use CoqIDE display menu instead
>
> I don't understand the motivation behind this.
Once again, a very pragmatic one : keeping the display menu and the
behavior synchronized ! It is a consequence of the naiveness of the
Coqtop - CoqIDE protocol. There is nothing done in order that coqide
knows the state of coq options. Consequently, CoqIDE imposes the options
set in the menu at each command !

When you want to send "Definition foo := bar." to coqtop thought CoqIDE.
You send "Unset Display Implicit Arguments. Unset Printing Coertion. Set
Printing ...... Definition foo := bar." in reality. So a litteral "Set
Printing All." is overwritten before any next command.

  The commands are quite useful when explaining Coq to beginners.  For 
instance, in the lecture notes we more than once have

Set Printing All.
Check TERM.
Unset Printing All.

That's true. I don't have any easy solution. And on the opposite, I think it 
musn't be user duty to know by head coq options and I don't like the 
impossed-by-emacs way of dealing with options. You should set or unset a 
printing setting, not undo its setting. I'm open to any suggestion/remark/...

I know that I can do Set and Unset through the display menu.


>  BTW, Compute is missing in the Queries menu.
True but commands of the query menu are the one that you are expect to
use by "selection with the mouse, shortcut" whereas Compute is not that
often used with something already written on screen. Anyway, it is very
easy to add it...
> Gert
All the best,
Pierre B.