50 Recent Changes in PG Web retrieved at 01:39 (GMT)

Statistics for nop PG Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save and ...
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 ...
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 ...
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 ...
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 ...
Web Web Home Changes Index Search
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 Testing For ProofGeneralEmacs, please see PGEmacsTestingNotes PGEmacs37Compatibility For PGIP based software, please see: ProofGeneralKitTesting ...
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 ...
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 ...
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 ...
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 ...
ProofGeneralUser 24 Feb 2008
Running Proof General on Windows to be written Meanwhile some pointers: Norbert Völker's on Windows/Cygwin page
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 ...
PGIP Development This page is intended for discussion on PGIP development. Once robust/tested, material here should be moved elsewhere, e.g.: PGIPRecentChanges ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
Notes on PGIP Meeting, Day Two Structure of history and synchronization Free navigation, with unlimited/unrestricted undo Supported in Matita ...
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 ...
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 ...
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 ...
Proof Engineering under construction Our definition of Proof Engineering is as the body of techniques conerned with the construction , maintenance , and understanding ...
Getting started with PG Eclipse to be completed (please help)
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 ...
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 ...
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 ...
Interface Concepts (Glossary) please help extend this glossary This page introduces some of the terminology used in the Proof General documentation. Theorem ...
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 ...
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 ...
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 ...
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 ...
This is to clarify current development branches and their locations. TODO(!) GrahamDutton 13 Sep 2006
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 ...
User contributed hints for using Proof General Emacs Please add hints and tips below (follow GoodStyle).
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 ...
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 ...
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 on implementing PGIP interface components Basically: 1. Support XML message passing over pipes/sockets 2. Implemement PGIP message dispatch and reception ...
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 ...
Proof General Kit General Kit is our implementation of the PGIP protocol and interface architecture. It consists of: A Haskell middleware component, the ProofGeneralBroker ...
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 ...
Number of topics: 50

See also: rss-small RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Topic revision: r4 - 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