The Coq mailing list

[Ramana Kumar <ramana.kumar AT gmail.com>]

On Wed, Jun 13, 2012 at 4:35 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> Thanks; that is a pretty good suggestion.  It has the downside of needing to
> commit to using a module at the point where the bad definition is made.  I
> think that reduces some of the educational value; I sometimes want readers
> to be _surprised_ when a definition doesn't work out. :)  I could hide the
> module commands, but then readers following along typing code from a
> document might get confused.  Also, it is unfortunate to have to introduce
> modules early in an introduction to Coq.  So, I'll still be grateful if
> someone has a further suggestion that avoids modules.

You could enclose everything in modules and treat it as a kind of
"necessary boilerplate (to be explained later)" from the educational
standpoint.
Does it make sense any more to, as an interactive user, write Coq code
without using modules?
I think the solution to Adam's problem should be something like what a
real user would do, because real users do sometimes get surprised when
a definition doesn't work out.
Do you then restart your IDE or step backwards through it or
something? Would it make sense for CPDT readers to be encouraged to
restart the IDE, but then continue from the point in the book where
they left off?

>
>
> On 06/13/2012 11:30 AM, Bruno Barras wrote:
>>
>>
>> You could use modules:
>>
>> Module Attempt1.
>>  ...
>> End Attempt1.
>> Module Attempt2.
>>  ...
>> End Attempt2.
>> ... (* now the preferred style *)
>>
>> That should provide more or less the same semantics as Reset, but in a
>> more structured way. Moreover, that lets you refer to older attempts from
>> the preferred style.
>>
>> Bruno.
>>
>>
>> On 06/13/2012 05:17 PM, Pierre Casteran wrote:
>>>
>>> Yes, I met the same problem while writing tutorials or material for
>>> Lectures.
>>> This pattern is useful for comparing various styles of definition.
>>>
>>> Pierre
>>>
>>> Quoting Adam Chlipala 
>>> <adamc AT csail.mit.edu>:
>>>
>>>> This is the new error message that Coq 8.4beta2 gives when using coqc to
>>>> process files that use commands like [Reset].  Unfortunately, I've been
>>>> relying on such commands in CPDT <http://adam.chlipala.net/cpdt/>, for
>>>> didactic typesetting of command sequences that would never be present in
>>>> polished source files in "real" projects.  For instance, I will 
>>>> introduce a
>>>> bad definition, work through examples showing why it is bad, and then
>>>> [Reset] and redefine it.
>>>>
>>>> Does anyone have suggestions on how to refactor to support 8.4beta2?
>>>>
>>>
>>
>>
>