CoqPIE: A Better IDE for Coq Proof Development
"Discover CoqPIE, an innovative IDE designed to enhance productivity in complex theorem development by streamlining tedious tasks. With features such as project management, dependency tracking, and proof step highlighting, CoqPIE revolutionizes the Coq workflow. Explore its research contributions, implementation details, and promising future tactics." (Characters: 500)
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
CoqPIE: A Better IDE for Coq Kenneth Roe and Scott Smith 8/22/2016 The Johns Hopkins University
Motivation Motivated by productivity issues in developing complex theorems My own DPLL proof has been the test case for this editor My goal is to reduce the time that many of Coq s tedious tasks take
Research contribution A tool for complex proof development An improved understanding of Coq productivity issues Modeling of common work flows Creation of functionality to support these work flows Manipulations of the Coq AST are a key part of much of the functionality
Proof workflow is tedious Invariant mergeTheorem1 mergeTheorem1aux1 mergeTheorem1aux2 mergeTheorem1aux9 mergeTheorem1aux9b mergeTheorem1aux3 mergeTheorem1aux4b mergeTheorem1aux4 mergeTheorem1aux5 mergeTheorem1aux6 mergeTheorem1aux7 mergeTheorem1aux8
Tool features Full project management Hierarchical browser Just click to view definition and proof step Dependency management Colors to highlight proofs that need to be updated All intermediate goal states cached Allows quick review of proof Difference highlighting Replay assist Tools for splitting proofs
Tool implementation Python based About 13000 lines of code Good scripting language for tactics Tkinter (Tk/Tcl) for UI
Results (so far) CoqPIE Tool is usable Actively being used for for DPLL verification CoqIDE and Proof General are not being used 2000+ of proof code developed with CoqPIE All areas except replay found to be useful I anticipate using replay as proofs get further developed
Future CoqPIE tactics Dead proof detection Lemma search Inter-theorem replay Eliminating hypotheses
Available on GitHub https://github.com/kendroe/CoqPIE
