TODO

This is a list of TODO items for PVS, really more of a wish list. It is currently in no particular order, and has preliminary assignments: SO - Sam Owre, NS - Shankar

• (SO, NS) Add UTF-8 characters, and make native strings

• (SO) End of focus marker in the file so that we don't have to wait for the whole file to typecheck in order to fix one small thing, but still preserving the content of the rest of the file.

• (SO) Finish proof frames

• (SO) Incremental typechecking: any declarations not, conservatively speaking, affected by an edit retain their status.

• (NS) Better Integration with Yices2 including quantifiers and models

• (NS) Completion of C code generation, and other improvements to both Lisp and C code generation

• (NS) Rust code generation

• (SO) Co-recursion and co-induction; code generation support for codatatypes

• (SO) Faster typechecking: dependent types and perhaps speeding up pseudo-normalize

• (NS) Faster rewriting through better indexing

• (NS) Smarter quantifier instantiation: we could use e-graph matching in Yices2 to suggest instantiations

• (SO) Move to case-insensitive allegro so we can make use of quicklisp packages

• (SO) Use quicklisp websockets, for both Allegro and SBCL

• (SO) Look into building PVS in other lisps, and do benchmarking on them

• (SO & NS) Update documentation

• (SO) Make something akin to speedbar for:

  • Libraries, PVS files, Declarations
  • Proof trees

• (SO) Proof interruption in TCP, etc.

• (SO) Proof sync with Emacs Proof buffer

• (SO) Extend PVSio to allow instantiating current theory, etc.

• (SO) epsilon concretization

• (SO) git usage within PVS

• (SO) unit testing both for lisp and PVS specs

• (SO) replace parser (with Bison?)

• (SO) replace ilisp with slime

• (SO) ilisp persistent history

• (SO) replace defsystem with ASDF

• (SO) PVS notebooks (e.g., jupyter)

• (SO) Collect visible definition names in current sequent, for expand completion

• (SO) redo .prf format, and modify prover to keep resolutions for refactoring and statistics

• (SO) finish XML for PVS proofs

• (SO) JSON for PVS files and proofs

• (SO) finish moving to JSON API for XML-RPC/Websockets

• (SO & NS) dimensional analysis

• (SO & NS) ontic types

• (SO) datatype generic functions

• (SO) TCCs in proofs when specs are modified

• (SO & NS) support for making TCCs into lemmas

• (SO) make sure Hypatia works in 7.1

• (SO) improved browing during proof

• (SO) show theory instance