I feel like there was a way to give up on obligations but can't remember the command.
AFAIK there is no way to give up on an open module, not sure if it would be useful (typically it would be used for a test like
Module M : T. (* stuff *) Fail End M. Giveup M.
It could also be useful for teaching material (if you don't want to save what you did in a "failed attempt" module.
I'm not sure the mess with the document structure (*) is worth the gain here. This kind of tests could be done better with using a different interface that is not the document, but something which understands document operations.
(*) think of tools such as editors etc... get much more complex once you have such non-structural stuff
I don't get it
What you don't get?
what mess is there?
What I don't like is to give stuff such as
Module M. .... End M. a sequential interpretation
The mess is that I can't see my document as something where
Module of mod_data * cmds is a constructor
now modules become global state transformers
so the tradeoff for me is not enough
as for a start, using what are supposed to be Coq documents to script tests seems wrong
we had a pretty interesting discussion about this the other day tho, for example how people work on Jupyter vs the way you work on Coq
But that's a subjective view, of course
Note that for example, the way I handle this stuff in the current version of my doc manager is that implicitly close every open struct
so I keep the "parenthesization"
cc @Jason Gross (who could also be interested in such a feature...)
so if the user writes
module M ... Bar. and doesn't close it, all the tools see and
End M. at the end.
Last updated: Feb 05 2023 at 19:29 UTC