Re: [PG-devel] Use cl-lib instead of cl
Here's another patch. This one is again more along the lines of mere cleanup. Its goal is to reduce the amount of work done in proof-site, so Emacs starts up a bit faster and is less impacted by the presence of PG in those sessions where PG is actually not used. Stefan 0001-Reduce-the-impact-of-proof-site-in-case-PG-is-not-us.patch Description: Binary data ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Use cl-lib instead of cl
>> Here's another, > `git am` doesn't like this one :'( Hopefully, the one below will go through better. Sorry 'bout the incomplete removal of cl.el as well. I made another round of checks and found a few more leftover uses. Stefan 0001-Cosmetic-cleanup-of-coq-smie-coq-syntax-and-coq-abbr.patch Description: Binary data ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Use cl-lib instead of cl
> Pushed as well. Thanks! [ Tant que je gagne, je joue! ] Here's another, Stefan >From 5549c4751e7e73382d2bd088322a483df90f51c9 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Thu, 13 Dec 2018 22:57:15 -0500 Subject: [PATCH] Fix remaining uses of CL; Make files more declarative MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f), so loading a file should "no effect". Fix the most obvious such effects: the splash screen and the autotests by moving those effects into a function. * coq/coq-autotest.el: Make it declarative. Use lexical-binding. (coq-autotest): New function holding the code that used to be at top-level. * generic/proof.el: Use lexical-binding. Don't call proof-splash-message just because we're being loaded. * generic/proof-script.el: Use lexical-scoping; fix all warnings. (pg-show-all-portions): Simplify the code with a closure. (proof-activate-scripting): Declare activated-interactively as dyn-scoped. (proof--splash-done): New var. (proof-mode): Call proof-splash-message upon first use. * generic/proof-splash.el (proof-splash-message): Don't check byte-compile-current-file now that we're only called when the mode is activated. * acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'. * coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²). * coq/coq-seq-compile.el: * coq/coq-par-test.el: * coq/coq-par-compile.el: Fix leftover uses of CL's `assert`. * generic/proof-utils.el: * generic/pg-movie.el: * etc/testsuite/pg-test.el: * coq/coq-syntax.el: Fix leftover uses of CL's `incf`. * generic/pg-autotest.el: Fix leftover uses of CL's `decf`. * obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use of CL's `loop`. * generic/pg-user.el (proof-add-completions): Do nothing if no proof-assistant is set yet (i.e. during byte-compilation). (byte-compile-current-file): No need to test this any more. * generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat. Remove unnecessary "\\(?:...\\)". (proof-regexp-alt): Redefine in terms of proof-regexp-alt-list. --- acl2/acl2.el| 9 ++--- coq/coq-autotest.el | 6 ++- coq/coq-db.el | 16 coq/coq-par-compile.el | 34 coq/coq-par-test.el | 35 + coq/coq-seq-compile.el | 5 ++- coq/coq-syntax.el | 17 etc/testsuite/pg-test.el| 8 ++-- generic/pg-autotest.el | 9 +++-- generic/pg-movie.el | 5 ++- generic/pg-user.el | 16 generic/proof-script.el | 96 +++-- generic/proof-splash.el | 4 +- generic/proof-syntax.el | 14 +++ generic/proof-useropts.el | 4 +- generic/proof-utils.el | 6 +-- generic/proof.el| 5 +-- obsolete/plastic/plastic.el | 4 +- 18 files changed, 147 insertions(+), 146 deletions(-) diff --git a/acl2/acl2.el b/acl2/acl2.el index cf9f521c..db3120ed 100644 --- a/acl2/acl2.el +++ b/acl2/acl2.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -24,10 +24,9 @@ (require 'proof-easy-config); easy configure mechanism (require 'proof-syntax) ; functions for making regexps -(setq auto-mode-alist ; ACL2 uses two file extensions - (cons; Only grab .lisp extension after - (cons "\\.lisp$" 'acl2-mode) ; an acl2 file has been loaded - auto-mode-alist)) +(add-to-list 'auto-mode-alist; ACL2 uses two file extensions + ; Only grab .lisp extension after + (cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded (proof-easy-config 'acl2 "ACL2" proof-assistant-home-page "http://www.cs.utexas.edu/users/moore/acl2; diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 8be4bed9..5ca66706 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -1,4 +1,4 @@ -;;; coq-autotest.el --- tests of Coq Proof General (in progress). +;;; coq-autotest.el --- tests of Coq Proof General (in progress) -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -21,7 +21,9 @@ (require 'proof-site) (defvar coq-compile-before-require) -(unless (bound-and-true-p byte-compile-current-file) +;;;###autoload +(defun coq-autotest () + (interactive) (pg-autotest start 'debug) diff --git a/coq/coq-db.el b/coq/coq-db.el index 36812c4c..7e59bffb
[PG-devel] Use cl-lib instead of cl (was: Supported version of Emacs)
>>> I'm happy to push it for you. Would you mind sending a copy as a `git >>> format-patch` attachment, so that the commit is properly attributed? >> Here it is, > Pushed, thanks. Looking forward to more neat patches :) Here's the next one. `cl` is deprecated in favor of cl-lib, which is virtually identical except it uses names with a "cl-" prefix, so this patch makes the corresponding change. It also uses lexical-binding in a few files (e.g. to replace lexical-let which was in `cl` but is not in `cl-lib`) and removes most of the (require 'proof-compat) since they're mostly unused. Stefan >From 4e1eec445658173273e11a49e0733250745278a4 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Wed, 12 Dec 2018 15:20:08 -0500 Subject: [PATCH] Use `cl-lib` instead of `cl` everywhere MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused. --- coq/coq-autotest.el | 5 +-- coq/coq-compile-common.el | 5 +-- coq/coq-db.el | 19 ++-- coq/coq-local-vars.el | 7 ++--- coq/coq-par-compile.el | 3 -- coq/coq-seq-compile.el | 3 -- coq/coq-system.el | 8 ++--- coq/coq.el | 53 +++ doc/docstring-magic.el | 3 +- easycrypt/easycrypt.el | 3 +- generic/pg-assoc.el | 7 +++-- generic/pg-goals.el | 1 - generic/pg-pgip.el | 20 ++-- generic/pg-user.el | 36 ++--- generic/pg-xml.el | 15 + generic/proof-depends.el| 15 + generic/proof-maths-menu.el | 5 +-- generic/proof-menu.el | 33 +++- generic/proof-script.el | 42 - generic/proof-shell.el | 30 +- generic/proof-syntax.el | 3 +- generic/proof-tree.el | 11 +++ generic/proof-unicode-tokens.el | 5 +-- generic/proof-utils.el | 1 - generic/proof.el| 5 ++- hol-light/hol-light-autotest.el | 5 +-- isar/isabelle-system.el | 5 ++- isar/isar-autotest.el | 3 -- isar/isar-profiling.el | 3 -- isar/isar-syntax.el | 10 +++--- isar/isar-unicode-tokens.el | 10 +++--- isar/isar.el| 3 -- lego/lego.el| 5 +-- lib/holes.el| 69 +++-- lib/pg-dev.el | 5 +-- lib/proof-compat.el | 4 +-- lib/span.el | 42 - lib/texi-docstring-magic.el | 5 +-- lib/unicode-tokens.el | 29 - obsolete/plastic/plastic.el | 24 +++--- 40 files changed, 252 insertions(+), 308 deletions(-) diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index cecfdcf1..8be4bed9 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -16,9 +16,6 @@ ;;; Code: -(eval-when-compile - (require 'cl)) - (require 'pg-autotest) (require 'proof-site) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 9dca0082..d29bf1b9 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -22,6 +22,7 @@ ;;; Code: +(require 'cl-lib) ;cl-every cl-some (require 'proof-shell) (require 'coq-system) (require 'compile) @@ -442,7 +443,7 @@ expressions in here are always matched against the .vo file name, regardless whether ``-quick'' would be use
Re: [PG-devel] Supported version of Emacs
> I'm happy to push it for you. Would you mind sending a copy as a `git > format-patch` attachment, so that the commit is properly attributed? Here it is, Stefan >From 1cd25fa20ccac27835b1609cfc089615aade2575 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 11 Dec 2018 18:48:51 -0500 Subject: [PATCH] Cleanup patch; Moving defvar to toplevel MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. --- .gitignore | 1 + coq/coq-compile-common.el | 9 ++--- coq/coq-indent.el | 5 +-- coq/coq-local-vars.el | 7 ++-- coq/coq-par-compile.el | 5 +-- coq/coq-seq-compile.el | 5 +-- coq/coq-system.el | 7 ++-- coq/coq.el | 72 +++-- generic/pg-goals.el | 8 ++-- generic/pg-response.el | 8 ++-- generic/pg-user.el | 9 ++--- generic/proof-autoloads.el | 2 - generic/proof-menu.el | 7 ++-- generic/proof-script.el | 8 ++-- generic/proof-shell.el | 10 ++--- generic/proof-site.el | 5 +-- generic/proof-utils.el | 9 +++-- hol-light/hol-light.el | 10 ++--- isar/isabelle-system.el | 5 ++- isar/isar.el| 9 +++-- lib/proof-compat.el | 80 + obsolete/plastic/plastic.el | 6 ++- pg-init.el | 25 +++- 23 files changed, 110 insertions(+), 202 deletions(-) diff --git a/.gitignore b/.gitignore index 9cd6d703..2039757e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,5 +2,6 @@ nohup.out TAGS ChangeLog +proof-general-autoloads.el *.elc *~ diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 97ea6ec6..9dca0082 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -26,10 +26,9 @@ (require 'coq-system) (require 'compile) -(eval-when-compile - ;;(defvar coq-pre-v85 nil) - (defvar coq-confirm-external-compilation); defpacustom - (defvar coq-compile-parallel-in-background)) ; defpacustom +;;(defvar coq-pre-v85 nil) +(defvar coq-confirm-external-compilation); defpacustom +(defvar coq-compile-parallel-in-background) ; defpacustom ; ;; diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 6e8ba013..af780251 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -33,8 +33,7 @@ ; ,@body ; (message "%.06f" (float-time (time-since time) -(eval-when-compile - (defvar coq-script-indent)) +(defvar coq-script-indent) (defconst coq-any-command-regexp (proof-regexp-alt-list coq-keywords)) diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index b8c5d7e3..f172adbe 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyrig
Re: [PG-devel] Supported version of Emacs
> Find below a first patch. Is there something else I need to do for this patch to be installed, or should I just wait a bit more (I have other patches in the pipeline after this one). Stefan > 2018-11-28 Stefan Monnier > > Move `defvar`s used to silence warnings outside of eval-when-compile. > Make sure they don't actually give a value to the var. > > * pg-init.el: Simplify. > Use (if t ...) to avoid running `require` at compile-time. > Don't add subdirs to load-path here since this code is never used. > (pg-init--script-full-path, pg-init--pg-root): > Inline their definition into their sole user. > > * generic/proof-utils.el (proof-resize-window-tofit): > Inline definitions of window-leftmost-p and window-rightmost-p previously > in proof-compat.el. > > * lib/proof-compat.el (proof-running-on-win32): Remove, not used. > (mac-key-mode): Remove, there's no carbon-emacs-package-version in > Emacs≥24.3. > (pg-custom-undeclare-variable): Use dolist. > (save-selected-frame): Remove, save-selected-window also saves > the selected frame at the same time. Update all users (which already > used save-selected-window around it). > (window-leftmost-p, window-rightmost-p, window-bottom-p) > (find-coding-system): Remove, unused. > > * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar > it to a dummy value and... > (hol-light): ...check its existence before using it instead. > > * coq/coq.el (coq-may-use-prettify): Simplify initialization. > > > > diff --git a/.gitignore b/.gitignore > index 9cd6d703..2039757e 100644 > --- a/.gitignore > +++ b/.gitignore > @@ -2,5 +2,6 @@ > nohup.out > TAGS > ChangeLog > +proof-general-autoloads.el > *.elc > *~ > diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el > index 97ea6ec6..9dca0082 100644 > --- a/coq/coq-compile-common.el > +++ b/coq/coq-compile-common.el > @@ -3,7 +3,7 @@ > ;; This file is part of Proof General. > > ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh > -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. > +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. > ;; Portions © Copyright 2001-2017 Pierre Courtieu > ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel > ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews > @@ -26,10 +26,9 @@ > (require 'coq-system) > (require 'compile) > > -(eval-when-compile > - ;;(defvar coq-pre-v85 nil) > - (defvar coq-confirm-external-compilation); defpacustom > - (defvar coq-compile-parallel-in-background)) ; defpacustom > +;;(defvar coq-pre-v85 nil) > +(defvar coq-confirm-external-compilation); defpacustom > +(defvar coq-compile-parallel-in-background) ; defpacustom > > ; > ;; > diff --git a/coq/coq-indent.el b/coq/coq-indent.el > index 6e8ba013..af780251 100644 > --- a/coq/coq-indent.el > +++ b/coq/coq-indent.el > @@ -3,7 +3,7 @@ > ;; This file is part of Proof General. > > ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh > -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. > +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. > ;; Portions © Copyright 2001-2017 Pierre Courtieu > ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel > ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews > @@ -33,8 +33,7 @@ > ; ,@body > ; (message "%.06f" (float-time (time-since time) > > -(eval-when-compile > - (defvar coq-script-indent)) > +(defvar coq-script-indent) > > (defconst coq-any-command-regexp >(proof-regexp-alt-list coq-keywords)) > diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el > index b8c5d7e3..f172adbe 100644 > --- a/coq/coq-local-vars.el > +++ b/coq/coq-local-vars.el > @@ -3,7 +3,7 @@ > ;; This file is part of Proof General. > > ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh > -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. > +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. > ;; Portions © Copyright 2001-2017 Pierre Courtieu > ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel > ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews > @@ -22,9 +22,8 @@ > (eval-when-compile >(require 'cl)) > > -(eval-when-compile > - (defvar coq-prog-name) > - (defvar coq-load-path)) > +(defvar coq-prog-name) > +(defvar coq-load-path) > >
Re: [PG-devel] Indentation tests
> You have something like that in Coq/ex/indent.v. > I dream of a smie with two grammars (and lexers): one for first lines of > commands and one inside commands. It would greatly simplify things I think. I don't really know how to define "first lines" and "inside", but you can definitely have "two grammars" with SMIE: You can combine two smie-grammars with something like (append (mapcar (lambda (x) (cons (concat "1" (car x)) (cdr x))) grammar1) (mapcar (lambda (x) (cons (concat "2" (car x)) (cdr x))) grammar2)) then you can combine the two tokenizing functions with: (defun combined-fun () (if (in-first-lines-of-commands) (let ((tok (fun1))) (if tok (concat "1" tok))) (let ((tok (fun2))) (if tok (concat "2" tok) this won't quite work right because: - the tokenizer can return nil for open/close parens and such in which case the above will fail to add the corresponding "1" or "2" prefix. - the relative precedence of the two grammars is left unspecified so it can lead to surprises when crossing between one part and the other. But neither of those two problems are hard to fix, I think. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Indentation tests
I have a few tentative changes to coq-smie.el. Does someone have some kind of test-suite somewhere against which I can run my new code to try and avoid regressions? Ideally, it should be fully automated, including fixing my bugs and outputting a Coq proof that the result is correct, but I'll settle for a long file that I need to reindent manually. So far I have the coq/indent.v but it doesn't seem to include some cases that are mentioned in coq-smie.el, so I'm hoping someone has something a bit more complete. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
> Now that you have mentioned it, we consider this pretty unoptimal and we > agreed on removing Coq from Debian due to the perils of shipping an > outdated version :( :( I find it perfectly adequate for my needs, FWIW. And I'd be annoyed to have to install Coq manually. 2 years old sounds like a really weird definition of outdated to me. To take a "random" example, ProofGeneral tries to be compatible with Emacs-24.3 which is 5 years old. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] SerAPI
Looking at SerAPI, I'm wondering about the choice of "sexp". I know it may sound odd to want something else than sexps when working in Elisp, but in reality sexps only work well if they use *exactly* the same syntax. E.g. in https://github.com/ejgallego/coq-serapi I see: (Query ((sid 3) (pp ((pp_format PpStr Goals) > (Answer 3 Ack) > (Answer 3 (ObjList ((CoqString > "\ >\n n : nat\ >\n\ >\nn + 0 = n" > (Answer 3 Completed) which seems to show that the strings don't use the same escape syntax as Elisp. This little detail will likely end up forcing the Elisp side to either re-implement a sexp-reader by hand (in Elisp, which will be slowish), or require ugly hacks to try and pre-process the answer before passing it to the sexp reader (or post-process the sexp), which will likely always end up flaky. Same thing when it comes to turning Elisp sexps into the print representation of SerAPI sexps, of course. This said, I don't see any hand parsing or pre/post processing tricks when reading SerAPI's sexps: I only see the prin1-to-sexp hack which works around the nil-vs-() difference. So maybe the syntax is closer to that of Elisp than shown in the README.md. Otherwise I see 2 convenient options: tweak the sexp syntax so it is a 100% subset of that of Elisp or use some other widespread standard such as XML or JSON (modern Emacsen can link to efficient parsers of those two). The first option is of course more convenient for Emacs, but I understand that the second is more convenient for all the non-Emacs clients and it's not that bad for Emacs. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
> I guess at some point it would make sense to tie PG to an specific Coq > range; I think the required changes could be made in the range of Coq >= > 8.8. FWIW, Debian stable has Coq-8.6 (which is only about 2 years old), so that's what I use on some of my machines. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
> In my opinion, it seems very likely that the branch will never reach a > working state; mainly because it would be hard to justify putting time > to fix it when you have other alternatives that allow a much lightweight > and robust implementation. I'm not up to speed on those alternatives. What would these be? Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
> Yes, exactly. `master` is still the mainline branch to integrate new PRs > while the nextgen implementation available in `async` is still in alpha phase. OK, good. > We'd specifically want to keep support of Emacs 24.3 for the moment > because this is still the version of the emacs24 package distributed > in Ubuntu 14.04 LTS: OK, thanks. Find below a first patch. I'd be interested to try out the `async` branch (and maybe help keep it up-to-date with `master`), but I can't get it to work (with Emacs and Coq from Debian stable). I understand it's work-in-progress, but is there a setup that's known to work, so I can try and detect regressions? Stefan 2018-11-28 Stefan Monnier Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. diff --git a/.gitignore b/.gitignore index 9cd6d703..2039757e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,5 +2,6 @@ nohup.out TAGS ChangeLog +proof-general-autoloads.el *.elc *~ diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 97ea6ec6..9dca0082 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -26,10 +26,9 @@ (require 'coq-system) (require 'compile) -(eval-when-compile - ;;(defvar coq-pre-v85 nil) - (defvar coq-confirm-external-compilation); defpacustom - (defvar coq-compile-parallel-in-background)) ; defpacustom +;;(defvar coq-pre-v85 nil) +(defvar coq-confirm-external-compilation); defpacustom +(defvar coq-compile-parallel-in-background) ; defpacustom ; ;; diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 6e8ba013..af780251 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -33,8 +33,7 @@ ; ,@body ; (message "%.06f" (float-time (time-since time) -(eval-when-compile - (defvar coq-script-indent)) +(defvar coq-script-indent) (defconst coq-any-command-regexp (proof-regexp-alt-list coq-keywords)) diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index b8c5d7e3..f172adbe 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -22,9 +22,8 @@ (eval-when-compile (require 'cl)) -(eval-when-compile - (defvar coq-prog-name) - (defvar coq-load-path)) +(defvar coq-prog-name) +(defvar coq-load-path) (defconst coq-local-vars-doc nil diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index
[PG-devel] Supported version of Emacs
I'm consider sending patches that change the code to take advantage of features from newer Emacsen (such as lexical-binding) but am wondering what's the "target" supported version. In the `master` branch (PG-4.5), it is claimed that it should work under Emacs-24.3 whereas in the `async` branch (PG-5.0) it says 24.4. On the surface this makes sense if we assume that `master` is legacy code that's in pure-maintenance mode. But I also see that `async` is based on PG-4.4.1 which said that it needed Emacs-24.4, and the `async` branch has not integrated the more recent changes to `master`, including those which apparently make it work under 24.3. So is the plan to merge the changes from `master` back into `async` (that would seem to make a lot of sense to me), and if so does that mean that `async` will want to work under Emacs-24.3 (and hence that in my patches I should try to avoid features that were introduced in 24.4)? Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Proof General's ability to interpret ANSI escape code from a proof assistant
> How difficult would it be for Proof General to support ANSI escape codes > (used to set color, bold, underline, etc.) embedded in the output of a proof > assistant? Depends on the details, but you can try to simply add a call to `ansi-color-apply-on-region compilation-filter-start` right after inserting the new text. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
> wiring M-x compile to "make vio2vo J=X" and then wiring that to a > shortcut is going to be simpler. (I didn't even know about M-x compile FWIW, I happily use (global-set-key "\C-c\C-c" 'compile) Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs
>> 2. Refactor PG to delimit new interfaces, and somehow support both the old >> REPL mode and the new async mode. >> 3. Refactor PG to use the new async mode, dropping the REPL and support for >> old proof assistants on the way. Actually, I think the best way to do 2 is to first do 3 and then see how to merge the new and the old. > There might be a tiny minority of Isabelle users who did not follow new > releases in the last 2 years and are still using Isabelle2014 with Proof > General. I don't see a problem with that: they just won't be able to > upgrade Proof General and remain stable on both. In an ideal world, the new PG Coq code should make it easier to support the "new" Isabelle API. It would be good for someone somewhat familiar with the "new" Isabelle API to keep an eye on the new PG Coq code (or for those working on the new PG Coq code to take a look at the "new" Isabelle API). Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
(add-hook 'proof-activate-scripting-hook '(lambda () (when As mentioned recently, the above (lambda ...) s-expressions is not data but is a function, so don't quote it with '. Stefan PS: As Elisp slowly moves to lexical scoping, the difference between the two is becoming more important, hence my renewed battle against such quoting. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Feature name conflict with Coq
Or by those who designed Emacs with a flat namespace for features and library files... Ahem! Please don't put .../ProofGeneral/coq in the load-path, and then simply do (require 'coq/coq). However, I believe it would be better if Coq and Proof General use different feature names. Because I have the impression, the Emacs mode distributed with Coq is rarely used, I would suggest that Coq changes the names of 'coq, 'coq-db and 'coq-syntax. Or supresses the installation of these files with the default make install. Another take on it is that the two teams should join their efforts. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
- lists of the form ('rec dir path) for -R dir -as path,
- lists of the form ('nonrec dir path) for -I dir -as path,
That sounds OK, except there shouldn't be quotes in there:
- lists of the form (rec dir path) for -R dir -as path,
- lists of the form (nonrec dir path) for -I dir -as path,
Stefan
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] ChangeLog branch chaos
default. There is no real fix, because cvs log cannot generate all information that belongs to a particular branch. Even Debian Actually, there is a real fix: convert the CVS repository to some other (saner?) format like Bazaar or Git, and then use those tools to get the change log for whichever branch you're interested in. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
