100 Recent Changes in PG Web retrieved at 23:44 (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 ...
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 ...
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
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 ...
Running Proof General on Windows to be written Meanwhile some pointers: Norbert Völker's on Windows/Cygwin page
This is an abbreviation for Proof General Emacs.
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 ...
Ideas discussed: New scheme for editing where display creates objects and informs prover of object deletions Maybe less efficient for "lazy displays" Something ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
The Isabelle CVS repository is available at: {{{ :pserver:anonymous@cvsbroy.informatik.tu muenchen.de/usr/proj/isabelle repository/archive }}} DavidAspinall 12 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
Proof Engineering under construction Our definition of Proof Engineering is as the body of techniques conerned with the construction , maintenance , and understanding ...
Tasks in PG Eclipse to be completed (please help)
Getting started with PG Eclipse to be completed (please help)
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 ...
Document markup with PGIP TODO Basic proof script elements; types, names, obj types Examples Annotation with metainformation elements
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 ...
Proof General Eclipse User Documentation Documentation is sadly lacking at present. Please request help on unclear areas (edit this page, adding your question), or ...
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 ...
Dynamic components/components with startup arguments Isabelle is started with isabelle logicname where logicname is chosen from a list of heap images in the ...
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 ...
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 ...
Plans for extending Proof General support in Isabelle These notes are based on discussions of DavidAspinall and MakariusWenzel at MKM2006. Extending Isabelle with ...
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 ...
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 ...
See (external) for details. GrahamDutton 14 Sep 2006
This is to clarify current development branches and their locations. TODO(!) GrahamDutton 13 Sep 2006
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 ...
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 ...
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 ...
About Mathematical Symbols in Proof General Currently: ProofGeneralEmacs relies on X Symbol ProofGeneralKit proposes PGML for simple symbol markup (cf HTML ...
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 ...
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 ...
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 ...
Testing Proof General Kit TODO: please add notes here
User contributed hints for using Proof General Emacs Please add hints and tips below (follow GoodStyle).
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 ...
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 ...
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 ...
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 ...
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 ...
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 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 ...
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 ...
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
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 ...
Proof General in Emacs: Working Platforms Proof General 3.6 form based submission here under construction, see PGEmacsGoodPlatformsForm
Projects related to Proof General Competition is healthy! Please add sections, notes and links below to describe related systems of interest for Proof General. ...
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 ...
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 ...
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 ...
Number of topics: 100

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