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

Topic revision: r2 - 03 Jun 2007 - 10:46:09 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies