The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, 2019-01-25 at 08:57 +0000, Soegtrop, Michael wrote:
> I can imagine that mathematicians/logicians get upset about such
> impure thoughts. But in the end nested lemmas are a hack to get work
> done and as long as it works in practice it is fine.

I'm all for trading purity for practicality, you are preaching to the
converted ;-)

More seriously the current code tried to exactly avoid being "different
in batch and single step mode" but, today, I'm convinced we should
weaken this requirement. In particular dependency tracking is not, and
probably will never be, perfect hence an interactive mode where some
document editions are accepted without rechecking everything that could
have been broken seems to be an acceptable compromise. For that we need
a good representation of the document at the prover side. It is
something we are working on (today the document is entangled with its
"checking schedule" and this is a pain).

About the need of a view of the document that is a refinement of the
actual text, e.g. where technical lemmas are hidden and can be only
found by inspecting special comments/proof steps... well I hope that
by switching to mainstream IDEs we could get that at a little cost.
Most of them already show your the classes, the methods and their
privacy status, I guess we could just piggy back on that.

Ciao
-- 
Enrico Tassi