CoqPIE: A Coq IDE Aimed at Improving Proof Development Productivity
Any Coq user who as attempted a non-trivial proof has found that the process is extremely tedious. The author after analyzing some of his own workflow in developing proofs identified a number of areas in which the proof development process could be improved. One key finding is that of developing a large proof (with many lemmas) often requires many iterations of revisions on the statement of the proof. Developing the proof script often reveals errors in the statement of the proof. Changing the statement then requires the proof to be replayed which is very tedious. We introduce a new IDE, CoqPIE that has all the functionality of Proof General or Coq IDE plus many new features to deal with workflow issues. For example, the IDE introduces tools to automatically re- play and update proof scripts. Our CoqPIE IDE consists of about 8500 lines of Python code. The tkinter library is used which connects Python to Tk/Tcl. The IDE includes its own parser for Coq syntax to implement incremental reparsing and dependency management. Other key innovations include full project management, pre-running an entire project and saving Coq output at each proof step for later reference, and many useful tactics to transform proofs.
The UI consists of a window with three views. The view on the left show an overview of the entire project . The first level of nodes are the files in the project. The second level are definitions in the file. For proofs, additional levels exist for the tactics used in the proof. The middle view displays the source file selected in the left view. The view on the right is similar to the Coq state window in Coq IDE and Proof General. It shows the current goal and hypotheses. However, instead of showing the state at the current processing point of Coq, it shows the state just after the selected definition or proof step from the treeview at the left.
Biography:
Kenneth Roe is a PhD student at Johns Hopkins. He returned to graduate school in 2010 after working in the industry for many years. With this work experience, he has a good understanding of the key challenges in developing commercial quality software. This understanding guides his research in formal methods. In addition, Kenneth Roe is an active iOS developer. He has a small business selling iPhone apps. His most successful app, Smart Recorder, has over 1,000,000 device installs and has over 40,000 regular users. He also does iOS development contracts and has many clients.