Demo of PG Eclipse: schedule

Here are some notes on things to demo in PG Eclipse.

• Getting going:
  • Proof project wizard; proof script wizard
  • Import: from file system, CVS checkout
• Eclipse concepts:
  • Workspace and projects
  • Views: selecting available views, moving windows, zoom
• Proof General specifics and instantiations of generic framework:
  • Editor with standard/PG features plus:
    • unicode symbols, popups, folding
    • standard Eclipse stuff: bookmarks, tasks
  • Problems view and markers
  • Searching
  • Proof object view
  • Proof navigator
  • Consoles - unfortunately hard to use, could provide auto-wrapping on input
  • Consoles for: debug, tracing, I/O log. Missing: syslog (error log view instead)

• General remarks: value of IDEs

• Many future ideas:
  • New SM metaphors: ruler for state + next command highlight; prove-as-you-type
  • Hyperlinking definitions to web/source files in session
  • Theory browser (cf Java browser)
  • Graphical dependency display (code already there; needs re-connecting)
  • Undo/redo (easy)
  • Non-linear management (harder, needs prover support)
  • Further tool integration (IsaPlanner , PG Tips, tags, assn gen)

• Realities:
  • Fine tuning and debugging needed (approx 6 months work)
  • Workstation needs horsepower (think 1 core for Eclipse)

-- DavidAspinall - 28 May 2007