search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
110 stars 9 forks source link

Trivially parsable proof state #112

Open david-christiansen opened 9 years ago

david-christiansen commented 9 years ago

Right now, when a development is incomplete, JonPRL dumps a description of the proof state as output. However, this is a bit difficult to parse. If it were in some kind of structured format, even just an s-expression or json with a string source position and a string proof state, then I could define a flycheck checker, which would allow the proof state to be presented as tooltips that appear automatically as you work with the file.

david-christiansen commented 9 years ago

This as opposed to the present "load and peer into compile buffer" interface

jonsterling commented 9 years ago

That would be much better! To start with, I can definitely give structured output which has the source position in one field, and the state in another. Then, later on, perhaps we can think of what kind of cool stuff we can do by adding further structure.

Right now, using JonPRL is a lot like using Twelf: as you say, you check the development, and then you inspect the output in the other window. It would be much cooler to have something along the lines of what you are suggesting...

david-christiansen commented 9 years ago

Perhaps just provide a command line switch "--ide" that causes the output to be formatted differently. That keeps accessibility for non-Emacs users, and also doesn't bias it for others.

Prob. JSON is better than S-expr, if you want to get support from other editors.