calebegg / proof-pad-classic

An IDE for ACL2
http://proofpad.org
GNU General Public License v3.0
21 stars 4 forks source link

Progress bar for proofs #34

Open calebegg opened 12 years ago

calebegg commented 12 years ago

I think the proof tree is basically useless. Except as a sort of progress bar so you can tell when the proof attempt is going south.

I'm thinking it should have a proved / total fraction displayed somewhere prominently alongside a progress bar. It's kind of crappy because the "progress" bar will probably go backwards sometimes, which isn't really what those are supposed to do.

Well, maybe not, actually; if the progress bar is subdivided into equal segments representing the top level nodes of the proof tree and then further subdivided lower down, like a one dimensional tree map, that could work. I don't know if it would be more or less useful than a progress bar that goes backwards sometimes.

calebegg commented 12 years ago

Oh man it should be like the Safari address bar thing, where the progress bar is embedded in the proof bar and sweeps down from the top.