An interesting idea. I've written an "active code" system for my blog, based on the excellent Pandoc ( http://chriswarbo.net/essays/activecode/index.html http:/

An interesting idea. I've written an "active code" system for my blog, based on the excellent Pandoc ( http://chriswarbo.net/essays/activecode/index.html http://chriswarbo.net/essays/activecode/index.html ) so I can write code inside my posts and have it executed during rendering. There's no requirement to do things that way, but it's certainly possible to write posts containing blocks of Coq code and blocks of shell code for compiling them, such that a failed compilation will abort the rendering. In fact, I'm doing that very thing right now! Although I'm rendering a PDF paper rather than a HTML blog post ;)