On 03/12/2018 12.15, Emilio Jesús Gallego Arias wrote: > Emilio Jesús Gallego Arias <e...@x80.org> writes: > >> - Isabelle / PIDE understands complete projects; >> - reliable async support and integration with external tools; >> - better error reporting and handling. > > Some more: on the fly checking, real completion, semantic folding; I'm > sure experienced Isabelle users can come up with some more tricks.
Got it, thanks. Plenty of nice stuff to look forward to in future versions of Coq! We've had some success on the F* side with keeping the protocol stable while adding new features. I think the trick is to be conservative in the design of the core protocol, attempting to future-proof it somewhat (for example, you and I agreed that returning a pair of regions to indicate which segments a change invalidates is a bad idea; instead, it's much better to return a list of all invalidated regions, so that a future version of Coq can be more precise about which regions a change invalidates). Then you very seldom have to change the core protocol; instead, most improvements are new queries or new options for existing queries. Clément.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
