The Coq mailing list

[Gérard Huet <Gerard.Huet AT inria.fr>]

Yes, this may seem surprising as being inconsistent with other commenting conventions.

Such comments are very useful, since they may be commented out of code/proofs in the language they are commenting.

Their paradoxical character comes from their being unable to bracket incomplete representations from the master language.

Conversely, they do not induce a restriction in the concrete representation of e.g. strings. A string "X*)*" is well-formed, without

escaping conditions for its "*)" substring, so there is no reason for an enclosing comment to be prematurely closed in ways inconsistent with abstract syntax that it is commenting. 

The strangeness feeling comes only from an untenable position that concrete (ASCII or UTF8) representation has priority over the abstract objects.

The correct point of view is that they are not universal comments, but comments relative to their meta-language representation, be it Caml or Coq.

To my recollection, It is Pierre Weis who defended and established this commenting convention for Caml.

Its Coq avatar is just a late manifestation.

GH

Le 11 avr. 2014 à 15:44, Cedric Auger <sedrikov AT gmail.com> a écrit :

If I remember well, comments can also be nested. Ie. if you write "(* foo (* bar *) baz *)", all that will count for a single comment. The "baz *)" part is considered to be commented. This behavior is the same as Ocaml one, but different from C programming language.

2014-04-11 14:49 GMT+02:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 11/04/2014 14:32, bhandalc AT tcd.ie wrote:

I noticed a bug in the CoqIDE commenting. If you begin quotations within a
comment that are not closed then the comment fails to close.

This is not a bug; this is on purpose. ``*)'' is not recognized inside quoted strings, even if such a string happens in a comment. That way, if one puts a well-formed Coq script in a comment, then one gets a well-formed (empty) script, even if there are strings in it.

Best regards,

Guillaume

--
.../Sedrikov\...