Results from PG web retrieved at 20:46 (GMT)

About Mathematical Symbols in Proof General Currently: ProofGeneralEmacs relies on X Symbol ProofGeneralKit proposes PGML for simple symbol markup (cf HTML ...
Hints on Adding nop PGIP Support to a Theorem Prover This page is intended as a rough HOWTO for adding PGIP support to a theorem prover. Apart from hints below ...
Alternative Undo Models in PGIP At present, the behaviour of undo inside the theorem prover is understood by the PGIPBasicProverModel. The idea is that a prover should ...
Annotated Bibliography of Related Work : in progress An attempt to make a list of important publications related to the field of user interfaces for theorem provers ...
PG Kit Broker development plans The PG Kit Broker has been implemented by ChristophLueth with some contributions from DavidAspinall. We welcome other contributions ...
Contact Us We can be contacted individually using email addresses from the wiki user name links (please remove the word SPAMNOT from that the wiki inserts to ...
Notes on the Coq undo and syntax mechansims reformat From email discussion with PierreCourtieu: On Fri, 25 Aug 2006 17:38:59 0100 David Aspinall wrote: Hi ...
Gripes about Eclipse (for PG Emacs users) You've been an Emacs user proving theorems in Proof General for more years than you care to mention. Now you're wondering ...
See (external) for details. GrahamDutton 14 Sep 2006
Interface Concepts (Glossary) please help extend this glossary This page introduces some of the terminology used in the Proof General documentation. Theorem ...
The Isabelle CVS repository is available at: {{{ :pserver:anonymous@cvsbroy.informatik.tu muenchen.de/usr/proj/isabelle repository/archive }}} DavidAspinall 12 ...
Plans for extending Proof General support in Isabelle These notes are based on discussions of DavidAspinall and MakariusWenzel at MKM2006. Extending Isabelle with ...
Proof General Kit Development Issues Notes on the development of ProofGeneralKit. See also PGIPDevelNotes. Issues An issue is a bug which has not yet become a feature ...
Christoph and David discussed adding meta variables on 2.7.09. Some remaks/questions: Why do we want to do this? presumably: to explain operational behaviour ...
Ideas discussed: New scheme for editing where display creates objects and informs prover of object deletions Maybe less efficient for "lazy displays" Something ...
Proof General Kit with Emacs Emacs users needn't be worried about the new implementation of Proof General, because it allows for a number of different front ends to ...
Hints about using Eclipse (for Proof General users) Here are some notes about Eclipse and pointers to other web sites that may be useful for those starting out using ...
Notes on the design of proof languages ( essay under construction: please do not comment/revise yet ) A proof language is a formal language for writing mathematical ...
Management of objects by displays can it be made easier? Here are some thoughts about some possible protocol/broker changes prompted by writing Emacs display (notes ...
On prover id and component id Presently, a prover is identified by an attribute prover id in display messages, which uniquely identifies the running instance ...
Dynamic components/components with startup arguments Isabelle is started with isabelle logicname where logicname is chosen from a list of heap images in the ...
This is to clarify current development branches and their locations. TODO(!) GrahamDutton 13 Sep 2006
Broker enabled version of PG Eclipse The broker enabled version of PGEclipse is on a side branch of the CVS (by Ahsan Fayyaz, tagged Uni Bremen Ahsan1 ). It enables ...
Bugs in Proof General Eclipse At the moment the important issues are mentioned in PGEclipseFixesNeeded, but many more are known. Unless you have a serious problem ...
Notes on building, running and releasing PG Eclipse These notes assume you have checked out the project source from CVS according to PGEclipseSources. You should ...
Change log for PG Eclipse This is the file CHANGE LOG.txt from the Proof General plugin package ed.inf.proofgeneral . Eclipse Proof General Developers' Change ...
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 ...
Hints and tips for development of Proof General Eclipse Use the Javadoc documentation See http://proofgeneral.inf.ed.ac.uk/Kit/eclipse/javadoc/ (warning: probably ...
Plans for Proof General on Eclipse This is some ideas for GrahamDutton to do for ProofGeneralEclipse. Timescale Oct Dec 2006 Work will now more closely resemble ...
PG Eclipse Developer Documentation For those brave souls who want to extend/improve the Proof General Eclipse plugin, please feel free to browse the sources and ...
Proof General Eclipse Feature Requests This wiki page is for making feature requests to the developers of Proof General Eclipse. You need to register on the wiki ...
PG Eclipse recent fixes This is taken from the file docs/RELEASE LOG.txt in the distribution. Please check the most recent distribution for a perfectly up to date ...
PG Eclipse: Summary of current Issues This is a list of issues with PG Eclipse which may be show stopper problems for users. Fixing these will allow Proof General ...
Future enhancements of Proof General Eclipse (Wish List) This page is for gathering ideas for improvements to Proof General Eclipse. The ideas here are for user ...
Getting started with PG Eclipse to be completed (please help)
Installing Proof General for Eclipse At the moment we aren't ready for prime time. The interface is usable for basic proof replay and simple editing. Compared ...
PG Eclipse Installation Problems and Fixes If you have had a problem that is not described here, please edit the page, adding a request for help. This page has been ...
FIXME: this content from old wiki and not fully converted yet Isabelle Beginners Tutorial using PG Eclipse These pages provide a quick and dirty introduction to using ...
General plans for Proof General on Eclipse Here are our plans for some next things to implement in ProofGeneralEclipse. For a higher level view on our goals, see ...
Preferences: File Associations This is a list of settings that determines which prover Proof General should start for each file type that it handles. Note that editing ...
Preferences: Symbol Support This toggles whether or not the output viewers attempt to convert ascii representations into symbols. e.g. with symbol support on, is ...
FIXME: content ported from old wiki, needs validating Prover Setup Documentation These pages describe how to setup Proof General Eclipse for a new theorem prover ...
Notes on ideas for refactoring PG Eclipse Here are some notes on ways we might improve the current structure of PG Eclipse. There are two main aims: 1. Really allow ...
Proof General for Eclipse: Screenshots Click on a screen shot to view full size. Starting Up and Getting Help Description A Welcoming introduction to ...
Sources for Proof General Eclipse If you'd like to help us develop and extend Proof General Eclipse, you'll want to get the sources. Unsurprisingly, you'll need to ...
PG Eclipse: Successes and Failures Please add entries to the tables below to document success/failure with our software. This is meant to help briefly highlight ...
The Symbol Table Editor This editor allows you to customise the way Proof General displays mathematical (and other) symbols. You can define new symbols\ , or edit ...
Tasks in PG Eclipse to be completed (please help)
Log of PG Eclipse test compiles DavidAspinall 20 Aug 2006
Proof General Eclipse User Documentation Documentation is sadly lacking at present. Please request help on unclear areas (edit this page, adding your question), or ...
User contributed hints for using Proof General Emacs Please add hints and tips below (follow GoodStyle).
Utilities for Proof General Eclipse TPWrapper TPWrapper is a simple java utility for networking a command line theorem prover (not: does not work for MS Windows) ...
Welcome to the all new Proof General Eclipse! (beta) Thank you for trying out Proof General Eclipse. We hope you will find it a valuable tool. Please help us to ...
This is an abbreviation for Proof General Emacs.
Compatibility for Proof General 3.7 Often after a release people find difficulties with particular combinations of software. To help avoid that as much as possible ...
Contributors to Proof General on Emacs The original developers were DavidAspinall, Healfdene Goguen, Thomas Kleymann, and Dilip Sequeira. Contributions have been ...
Tips for Debugging Proof General This is based on the file etc/debugging tips.txt distributed with Proof General. Set the debug flags If Proof General gives an ...
Proof General in Emacs and Eclipse Currently less functionality thatn ProofGeneralEmacs But... prettier windows, advanced IDE environment... Will become ...
Proof General in Emacs: Working Platforms Proof General 3.6 form based submission here under construction, see PGEmacsGoodPlatformsForm
Good platforms form for PG Emacs Note: This is a maintenance topic, used by the TWiki administrator. This form defines data entry for the table at PGEmacsGoodPlatforms ...
Installation issues with Proof General Emacs This page is for information to help with installation of Proof General. These go beyond the details on the download ...
Running Proof General 4.0 on Mac OS X As of Mac OS 10.4, the Apple supplied version of Emacs only runs in a terminal window. This will provide only a primitive environment ...
Running Proof General on Windows to be written Meanwhile some pointers: Norbert Völker's on Windows/Cygwin page
Running Proof General on Windows XP Using Cygwin This is the recommended way to get things working. Visit http://www.cygwin.com/ to find out more. Using Coq Emacs ...
Outstanding Problems with PG Emacs This is a list of known problems which are not mentioned in the Proof General or http://proofgeneral.inf.ed.ac.uk/BUGS Known ...
Testing Proof General on Emacs Unfortunately there isn't a fully developed automated test mechanism yet. A basic set of tests is to try the following: 1. Check ...
Hints and tips for users of Proof General for Emacs Removing GUI clutter for Keyboard Purists I just spent a bunch of time getting rid of menu/tool/scroll bars on ...
Wanted Features for Proof General in Emacs Please add your ideas/votes to suggested features below, in each of the categories. Additional Support for Existing Provers ...
PG Kit Filespace Handling The current handling of files is that we quietly assume that the broker and the display live in the same filespace, as otherwise the user ...
PGIP, the Proof General Interaction Protocol PGIP is a protocol for conducting interactive proof and a framework for connecting theorem provers to interfaces and other ...
PGIP2 In order to integrate functionalities provided by the PLATO system insider PGKit, we have developed a specification for the next version of PGIP, currently called ...
PGIP2 Roadmap On this webpage we describe a roadmap how to smoothly move from the current PGKit implementation towards integrating the new features and concepts ...
PGIP Basic Model of Incremental Development PGIP understands that the theorem prover may be in one of four possible states while incrementally processing a proof script ...
PGIP Commentary The commentary on the PGIP syntax specification explains the meaning of PGIP commands. It is available as a file on the main PG kit page, http://proofgeneral ...
PGIP Development This page is intended for discussion on PGIP development. Once robust/tested, material here should be moved elsewhere, e.g.: PGIPRecentChanges ...
Hints on implementing PGIP interface components Basically: 1. Support XML message passing over pipes/sockets 2. Implemement PGIP message dispatch and reception ...
Document markup with PGIP TODO Basic proof script elements; types, names, obj types Examples Annotation with metainformation elements
Notes on PGIP support for PML DavidAspinall 19 Jun 2007 Use cases for PML Requirements: showing syntax and typing errors editing of a hole editing ...
Notes on PGIP next steps Here are some notes on desirable next steps for improving the emerging PGIP support in provers. Parse markup General idea: basic markup ...
PGIP Meeting agenda Some discussion points: Simplification of PGIP protocol: see PGIPVersionThree Unicode everywhere: MakariusW says: let's see again in ...
Agenda for Meeting at TUM to discuss PGIP, March 2007 DavidAspinall, ChristophLueth, CezaryKaliszyk will visit MakariusW. David will give a talk on Thu 14:00 ...
Older changes to PGIP This file provides some description of changes in the PGIP schema. Names and types for blocks in document The openblock element has two ...
Recent changes to PGIP Some recent changes and outstanding requests for change are included in Trac. Additional notes may be added below for items not included in ...
Road map for future PGIP releases 2.1 PGIP as it is now, in time for and compatible with Isabelle 2007, but with some simplifications to cut down on the number ...
Version 3.0 of PGIP Here are some collected ideas for the next major version change in PGIP. General The general aims of the revisions are: To make the protocol ...
PG Kit Developers Eclipse plugin ProofGeneralEclipse was developed by Winterstein with additional code by AlexHeneveld. AhsanFayyaz added support for the PGBroker ...
Proof General Kit Development Development information (general) Development information for Proof General Kit is spread among other topics: ProofGeneralBroker ...
Project ideas for PG Kit PGML Viewer A component that displays the PGML output from the prover for proofs in progress. Small window that can be duplicated with a ...
PGML, the Proof General Markup Language PGML is a simple markup language which was designed for Proof General to contain elements for describing mathematical symbols ...
Notes on PGIP Meeting, Day Two Structure of history and synchronization Free navigation, with unlimited/unrestricted undo Supported in Matita ...
Suggested in a mail from 13 May 05 by David: Detecting changes: "buffer modified tick". At the moment we talk about file modified status but not the Broker memory ...
New objects are not always new Sometimes, the broker needs to report the existence of objects which are not new: when asked to do so by display, or when asked to load ...
Suggested by David in a mail from 13 May 06: Discarding changes: revert/reload file. Actually what I want here is to revert to the Broker's in memory version, by ...
David suggested this in an email from 13 May 06: But I'm wondering what to do with asynchronous edits in the display that take place while we are waiting for the ...
PGWin: a desktop for theorem proving PGWin is based on the ideas of the IsaWin Isabelle interface. It is being reimplemented for the ProofGeneralKit architecture ...
The Stateless Display Protocol To rephrase the display protocol in a less stateful way (along the lines of the REST style), we categorize the existing messages into ...
Connecting PLATO and Proof General I had some discussions in Edinburgh in August 2006 about the possibility of connecting Proof General with the PLATO component of ...
Proof Engineering under construction Our definition of Proof Engineering is as the body of techniques conerned with the construction , maintenance , and understanding ...
Proof General Broker The Proof General broker is the middleware component of the Proof General Kit. It is implemented in Haskell. Installing the Broker Download ...
Style sheets for Proof General wiki attached here. DavidAspinall 19 Aug 2006 patternmods.css: patternmods.css
Proof General CVS Repository See http://proofgeneral.inf.ed.ac.uk/devel For all the ProofGeneralKit work, you need to checkout Kit instead of ProofGeneral
Development of Proof General Please see http://proofgeneral.inf.ed.ac.uk/devel for the main development page. New development is centred around a common protocol for ...
Proof General Eclipse Eclipse is an open source IDE originally developed by IBM. It started as a Java development environment, but has been re engineered to be a general ...
imported from old wiki, not really used here Welcome to Proof General Good interfaces and development tools are crucial if interactive proof systems are to be ...
Proof General in Emacs The 4.0 release of Proof General Emacs provides a front end based on Emacs. Please see the main web pages at http://proofgeneral.inf.ed.ac.uk ...
Proof General Kit General Kit is our implementation of the PGIP protocol and interface architecture. It consists of: A Haskell middleware component, the ProofGeneralBroker ...
Testing Proof General Kit TODO: please add notes here
Proof General Testing For ProofGeneralEmacs, please see PGEmacsTestingNotes PGEmacs37Compatibility For PGIP based software, please see: ProofGeneralKitTesting ...
Using Proof General Most users are using the current ProofGeneralEmacs software. Some useful pages are: PGEmacsUserHints user contributed hints, tips and patches ...
A REST view on the Broker Although a proof in progress is dynamic, we can structure URLs using a static format, e.g. http://localhost:7007/Example.thy/proofsteps ...
Projects related to Proof General Competition is healthy! Please add sections, notes and links below to describe related systems of interest for Proof General. ...
Systems related to Proof General in progress Here are some pointers to systems related to Proof General and brief notes on their features. We're mainly interested ...
Use cases for editing Various race conditions in displaybrokerprover We want to allow flexibility but be careful in case of race conditions. Example: 1. The user ...
Proof General Teacher View The Teacher View is a web browser for viewing tutorials that link to Proof General. These can activate certain functions within\ Proof ...
Technical Tidbits Here are some little works in progress that contain some technical challenges. Please us a shout or add notes here in case you can get things working ...
ProofGeneralUser 24 Feb 2008
The Isabelle Theorem Prover Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools \ for proving ...
Interactive Theorem Provers and Proof General Proof General is designed to support interactive theorem provers that have a particular architecture. Supported theorem ...
Dates 08 Jun 2007 11 Jun 2007 Ewen: Long weekend 04 Jun 2007 07 Jun 2007 David: Dublin 11 Jun 2007 14 Jun 2007 David: INRIA 15 Jun 2007 ...
Unicode Tokens replacement for X Symbol A replacement for X Symbol will be shipped with Proof General 4.0. This page makes some notes about its development. UnicodeTokensCutAndPaste ...
Copying with tokens Coping text "as Unicode" (Tokens Copy as Unicode) makes it readable in Unicode editors, web pages etc. Here's an example: text { "weak" typing ...
Welcome to the Proof General Wiki! This wiki is for collaboration on the use and development of General. To avoid spam, this wiki only allows editing by registered ...
Web Web Home Changes Index Search
TWikiGuest example #64;yourREMOVE THIS.company .WebChangesAlert, .TWikiRegistration
nop PG Web Preferences The following settings are web preferences of the PG web. These preferences overwrite the site level preferences in . and , ...
" else " nop TWiki's nop PG web"}% /PG
Statistics for nop PG Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save and ...
TODO for this Wiki Fix/complete porting content from old wiki Fix CommentPlugin css style seems to be broken/missing? Add more content for PG ...
X Symbol on Mac OS X, natively There are at least two nice native ports of GNU Emacs for Mac OS X: Emacs and Aquamacs. These work well with Proof General except for ...
Number of topics: 137

See also the faster WebTopicList

Topic revision: r5 - 15 Nov 2006 - 19:43:52 - TWikiContributor
 
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