From 4162624976e6339d0a835f8ab3d213da29f63647 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 24 Jun 1999 14:57:10 +0000 Subject: Updates for new web pages, todo list. --- AUTHORS | 25 +++++++++++-------------- CHANGES | 2 ++ COPYING | 2 +- Makefile.devel | 18 ++++++++++-------- README | 8 +++++--- todo | 31 ++++++++++++++++--------------- 6 files changed, 45 insertions(+), 41 deletions(-) diff --git a/AUTHORS b/AUTHORS index 6a30ec35..3816baf0 100644 --- a/AUTHORS +++ b/AUTHORS @@ -1,21 +1,18 @@ --*- outline -*- +Current Authors/Maintainers: -* Current Authors/Maintainers -** David Aspinall + David Aspinall doc, etc, generic, html, images, isa -** Patrick Loiseleur + Patrick Loiseleur coq -** Markus Wenzel + Markus Wenzel isar -** Paul Callaghan - plastic + Paul Callaghan + plastic, lego -* Previous Authors: -** Thomas Kleymann - lego, doc, generic -** Healfdene Goguen - coq, generic, doc -** Dilip Sequeira - lego +Previous Authors: + + Thomas Kleymann (lego, doc, generic) + Healfdene Goguen (coq, generic, doc) + Dilip Sequeira (lego) diff --git a/CHANGES b/CHANGES index 242f7a3f..4fb76c9c 100644 --- a/CHANGES +++ b/CHANGES @@ -23,6 +23,8 @@ Summary of Changes for Proof General 2.1 * Improvements to Coq mode: better recognition of Coq syntax, support for proof-shell-restart-cmd. +* Toolbar can now be switched on and off via menu. + * Bug fix for templates in Isabelle theory file mode. * Bug fix for long-lines with funny characters causing diff --git a/COPYING b/COPYING index cd626661..313f9451 100644 --- a/COPYING +++ b/COPYING @@ -1,4 +1,4 @@ -Proof General is Copyright (C) 1998 LFCS. +Proof General is Copyright (C) 1998,1999 LFCS. You are allowed to freely copy and modify this software for non-commercial use, providing you observe these diff --git a/Makefile.devel b/Makefile.devel index 1f283a54..62bab01f 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -50,10 +50,12 @@ # Release tag. For pre-releases. Watch out with -# substitution in tag target below, which edits -# html/download.html +# substitution in tag target below, which edits $(DOWNLOADHTML) PRERELEASE_TAG=2.1pre$(shell date "+%y%m%d") +# html/download.phtml +DOWNLOADHTML=download.phtml + # This is used for full releases to control the tag name # and distribution name. No editing of html is done @@ -95,7 +97,7 @@ TAR=tar DEVELMAKE=make -f Makefile.devel # Files not to include the distribution area or tarball -NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML plastic/ isar/ +NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML html/notes.txt plastic/ isar/ # Files not to include in the distribution tarball IGNOREDFILES=doc/ProofGeneral.dvi Makefile.devel todo isa/wip.ML @@ -218,7 +220,7 @@ images: FORCE ## ## tag: tag the CVS sources of working directory with CVS_RELEASENAME, ## set version stamp in proof-site.el and ProofGeneral.spec -## to VERSION, and edit download.html if VERSION matches +## to VERSION, and edit $(DOWNLOADHTML) if VERSION matches ## PRERELEASE_TAG. ## tag: @@ -227,18 +229,18 @@ tag: @echo "*************************************************" if [ -n "`cvs -n -q update`" ]; then exit 1; fi # Tag proof-site.el and ProofGeneral.spec - (cd generic; mv proof-site.el proof-site.el.old; sed -e 's/defconst proof-version \".*\"/defconst proof-version \"Proof General, Version $(VERSION) released by da,tms. Email proofgen@dcs.ed.ac.uk.\"/g' proof-site.el.old > proof-site.el; rm proof-site.el.old) + (cd generic; mv proof-site.el proof-site.el.old; sed -e 's/defconst proof-version \".*\"/defconst proof-version \"Proof General, Version $(VERSION) released by da. Email proofgen@dcs.ed.ac.uk.\"/g' proof-site.el.old > proof-site.el; rm proof-site.el.old) (cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/Version:.*$$/Version: $(VERSION)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old) -# Edit download.html only for prereleases. +# Edit $(DOWNLOADHTML) only for prereleases. # Careful: the sed command below relies on previous value of PRERELEASE_TAG. if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \ - (cd html; mv download.html download.html.old; sed -e 's|ProofGeneral-2\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' download.html.old > download.html; rm download.html.old) \ + (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ fi # This hack to SOURCE: name is only needed because we have an obsolete version # of rpm installed on standard machines at dcs.ed, and we have to build with # that version. Otherwise we could use the %{version} macro in the spec file. (cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/ProofGeneral-.*.tar.gz/$(RELEASENAMETARGZ)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old) - cvs commit -m"Set version tag for new release." generic/proof-site.el html/download.html etc/ProofGeneral.spec + cvs commit -m"Set version tag for new release." generic/proof-site.el html/$(DOWNLOADHTML) etc/ProofGeneral.spec cvs tag "$(CVS_RELEASENAME)" ############################################################ diff --git a/README b/README index 9c528edc..67f64b39 100644 --- a/README +++ b/README @@ -10,15 +10,17 @@ Please help us with this aim! Configure Proof General for your proof assistant, by adding features at the generic level wherever possible. Send ideas, comments, patches, code to proofgen@dcs.ed.ac.uk. - See INSTALL for installation details. See COPYING for license details. See doc/ for documentation of Proof General. +For the latest news and downloads, check the Proof General web page +at: http://www.dcs.ed.ac.uk/home/proofgen + -David Aspinall & Thomas Kleymann -November 1998. +David Aspinall. +July 1999. diff --git a/todo b/todo index 91755348..55cfecd9 100644 --- a/todo +++ b/todo @@ -25,18 +25,6 @@ A Clarify licence situation for Proof General after question from currently [22 Jan 1999] being drafted by UNIVED. Will wait for this (at least) before releasing 2.1. -B Add a "register" page for registering downloads. Perhaps filling - will be mandatory for users in a non-academic environment. - Suggestion: send an email to proofgen@dcs.ed.ac.uk with POST - results. Template: - http://www.dcs.ed.ac.uk/home/da/Isamode/IsamodeSurvey.html - [2 hours] - -B Make a mailing list for Proof General users. - [2 hours for introductory messages, mentioning on web - pages, understanding Majordomo. Maybe support will - make the list itself.] - B Polish ProofGeneral.texi and publish LaTeX version as an LFCS Technical Report. @@ -63,6 +51,10 @@ A BUGS to investigate: A Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. +B CVS repository issues. + Where are obsolete 'fileattr' files generated from/maintained? + Should junk these (which appear to say that tms is watching everything). + B QUESTION: why do we have proof-shell-proof-completed-regexp's perhaps objectionable behaviour of forcing the response buffer? Would it be safe just to set the proof-shell-proof-completed flag @@ -332,6 +324,10 @@ D Display management is much better than it was, but perhaps D Fixup display of urgent messages in minibuffer: split at newlines so we don't get ^J's in FSF Emacs. +D Make wellclean target remove images in html/images which are + generated from the image directory. Consider putting all the + image sources in images/ + X Is it possible to let C-c C-c (SIGINT) issue additional process input? Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or rather, to fail gracefully. @@ -548,12 +544,12 @@ X Sections and files are handled incorrectly. * Here are things to be done to Isabelle Mode ============================================= -A auto-adjust Pretty.setmargin when window is resized - A Multiple files needs careful testing. There are cases when retracting asks for files to be removed which were never loaded. This might be harmless, but might be better cleaned up. +B auto-adjust Pretty.setmargin when window is resized + C derive an isa-response-mode from proof-response-mode; see lego.el (10min) @@ -572,7 +568,8 @@ X Add ability to choose logic. Maybe not necessary: can use default (ponder this) X Write perl scripts to generate TAGS file for ML and thy files. - (6h, I've completely forgotten perl), or better: + (6h, I've completely forgotten perl). Does anyone + actually want this? X Manage multiple proofs (markers in possibly different buffers) @@ -587,6 +584,7 @@ C `proof-zap-commas-region' does not work for Emacs 20.2 on C proof-shell-dont-show-annotations doesn't seem to work. + * Bugs in other packages beyond our control =========================================== @@ -597,6 +595,8 @@ contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" * Stable version release checklist ================================== +0. Make all files have same CVS branch with cvs commit -f + (only seems to work locally, not via cvs server). 1. Test multiple file test suite for LEGO, Isabelle. Coq example. 2. Check case with FSF Emacs 3. Check case with compiled code, for XEmacs only. @@ -607,6 +607,7 @@ contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" cd doc; make magic 6. Update Emacs versions in texi, html/ 7. Check web page references from other places. +8. Validate web pages if they're changed much. -- cgit v1.2.3