Re: [PG-devel] Supported version of Emacs
On 11/12/2018 18.52, Stefan Monnier wrote: >> 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 :) signature.asc Description: OpenPGP digital signature ___ 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'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 © Copyright 1994-2012 David
Re: [PG-devel] Supported version of Emacs
On 11/12/2018 16.26, Stefan Monnier wrote: > Is there something else I need to do for this patch to be installed 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? Clément. signature.asc Description: OpenPGP digital signature ___ 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
> 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) > > > (defconst coq-local-vars-doc nil > diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el > index e3daebcd..b03fedaa 100644 > --- a/coq/coq-par-compile.el > +++ b/coq/coq-par-compile.el > @@ -3,7 +3,7 @@ > ;; This file is part of Proof General. > > ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh > -;; Portions © Copyright
Re: [PG-devel] Supported version of Emacs
On 03/12/2018 12.15, Emilio Jesús Gallego Arias wrote: > Emilio Jesús Gallego Arias writes: > >> - Isabelle / PIDE understands complete projects; >> - reliable async support and integration with external tools; >> - better error reporting and handling. > > Some more: on the fly checking, real completion, semantic folding; I'm > sure experienced Isabelle users can come up with some more tricks. Got it, thanks. Plenty of nice stuff to look forward to in future versions of Coq! We've had some success on the F* side with keeping the protocol stable while adding new features. I think the trick is to be conservative in the design of the core protocol, attempting to future-proof it somewhat (for example, you and I agreed that returning a pair of regions to indicate which segments a change invalidates is a bad idea; instead, it's much better to return a list of all invalidated regions, so that a future version of Coq can be more precise about which regions a change invalidates). Then you very seldom have to change the core protocol; instead, most improvements are new queries or new options for existing queries. Clément. signature.asc Description: OpenPGP digital signature ___ 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
Emilio Jesús Gallego Arias writes: > - Isabelle / PIDE understands complete projects; > - reliable async support and integration with external tools; > - better error reporting and handling. Some more: on the fly checking, real completion, semantic folding; I'm sure experienced Isabelle users can come up with some more tricks. ___ 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
On 03/12/2018 11.57, Emilio Jesús Gallego Arias wrote: > In the first case, my opinion (and the one of quite a few of my > colleagues) is yes, clearly ahead. But can you give concrete examples of extra features that they have? And, re the coupling, are these worth being stuck with a single editor? signature.asc Description: OpenPGP digital signature ___ 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
Le lun. 3 déc. 2018 à 13:11, Emilio Jesús Gallego Arias a écrit
:
>
> I feel like this may be the moment to make it a bit more "stable".
Good news!
> However, I would expect adding PG support to SerAPI to require at least
> one or two Coq releases where it would be marked "experimental" and thus
> subject to change.
Of course.
> IMHO we want to leave space to fix / improve / evolve aspects of the
> protocol before declaring it "stable".
>
> In fact, "stability" may be a diffuse notion when advanced features are
> needed, and I would dare to say that a futile goal in state of the art
> IDE/UI.
Of cours evolution is equally important. Please correct "stable" by
"backward compatible". The changes should not make valid commands
become invalid, or at least before having it tagged "obsolete" for
several years. Actually coq has a very good policy about backward
compatibility for *commands*, it should be exactly the same for
protocol commands (Add, Edit,...).
> For example, I understand Isabelle doesn't have any stability guarantee
> on the protocol level, thus they have to couple the IDE with the prover.
Yes this is the exact opposite of what the coq team is aiming at. So
the compatibility policy should not be the same.
> > This is important. I don't want to switch to a protocol that will not
> > be backward compatible for a long time. By long time I mean >= 10
> > years.
>
> While I understand and I am indeed sympathetic to that position, I would
> be quite worried if in 10 years it turns out we are using the same IDE
> protocol than we are using today. Likely by then, most Coq users would
> have switched to a different system that would provide them with more
> advanced functionality.
Enriching the protocol is not a problem (and should far enough for 10
years of new features I guess), but if you say all of a sudden: "the
sexpr now take curly brackets", or "the command Add takes one more
mandatory argument" or "now the protocol is sent with reverse polish
notation to avoid parenthesis" then everything breaks and every tool
based on your protocol is forced to do gory checkup at start or be
incompatible with older coq versions.
> Maybe I got confused by the "all" quantifier, but I see quite a few
> "other technologies" alive and doing pretty well.
I consider "dead" an ide that cannot follow coq's release cycle
(because people will switch to another one), and I consider as
"overheating" IDEs the ones that do not support coq beta versions
within a month:
From https://coq.inria.fr/related-tools:
"
The Proof General Emacs/XEmacs interface by David Aspinall with Coq
support by Pierre Courtieu; works for v8.9beta and master and at
least from v8.4
The Coqoon Eclipse plugin for Coq development (based on Wenzel's
asynchronous PIDE framework); Support for v8.7 and
v8.8 is highly experimental
The Coq PIDE Jedit (proof of concept) plugin for Coq development (also
based on asynchronous PIDE framework); * DEAD
the ProofWeb online web interface for Coq (and other proof
assistants), with a focus on teaching; *** DEAD (Welcome to
Coq trunk (Nov. 2006))
the PeaCoq online web interface for Coq (by Valentin Robert);
*** officially supports 8.5. There is v8.8 branch but not a lot of
things commited in it, lack of dev time?
ProverEditor is an experimental Eclipse plugin with support for Coq;
* DEAD
"
**More Found in cocorico:
"
vscoq A Visual Studio based interface developed in 2016. *** README
says "v8.5" ? supports probably 8.8.
jscoq A port of Coq to the browser; runs standalone using js_of_ocaml.
** looks up to date except for v8.9beta
CoqTail CoqTail is a vim plugin aiming to bring the interactivity of
CoqIDE into your favorite editor. ** looks up to date except for
v8.9beta
"
So:
1) more deads than alives
2) the only officially supporting ides for v8.9 currently are coqide
(with a problem with opam) and pg.
3) the last three are very promising BUT they are in a critical
moment: will they adapt easily to v8.9?
Note that 8.9 and master compatibility took 0 commit in pg. Of course
new features may not be supported at first but *at least* one can play
old proofs with the new coq. I remember having to support the new
"[goalid]: {" syntax. I am not sure I
I think your work on protocols is great, please take all this as
passionate comments. I do really want to see more tools around and you
are by far the one who contrinbutes the most to that purpose.
Best
Pierre
>
> > 1) almost no effort was needed to keep things working 2) each pg
> > version worked for several versions of coq spanning over 5 years at
> > least. This second point is not significant for coqide since it is
> > distributed with coq but it is a huge problem for other IDEs.
>
> > The protocol seems very nice and would greatly simplify pg's code but
> > I am not going to invest time on it if it is not guaranteed to be
> > still working in 10 years. I would better stay with the old and rough
> > REPL
Re: [PG-devel] Supported version of Emacs
I agree. One more argument: opam has problems and having Coq delivered only by opam is risky these days. So having a reliable fallback is good. Even if it is a bit outdated. P Le sam. 1 déc. 2018 à 03:53, Stefan Monnier a écrit : > > 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 > ___ 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
Re: [PG-devel] Supported version of Emacs
Pierre Courtieu writes: > I am all for it, where can I find the serapi documentation please? That's a good point, the documentation is fairly sketchy as we didn't see the need to make the API stable yet. In fact one of the problems Paul has pointed out was lack of specification of the XML protocol [which was 100% undocumented when the effort started IIRC] I will add some specification for the 8.9 version, any recommendation on to best document such a protocol? As the protocol is programmatically derived from https://github.com/ejgallego/coq-serapi/blob/v8.9/serapi/serapi_protocol.mli I think I will use OCaml's `odoc` format. Binaries command line is reasonably documented with --help. Cheers, E. ___ 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
"Paul A. Steckler" writes: > That helps a bit for some issues, but I think most of the bugs in the > async branch mostly relate to maintaining unstated or unknown > invariants in the implementation. Umm, I'm not sure I share that view, I'd dare to say that for a start the new protocol would allow to drop 90% of the code, and after all I don't see a reason things wouldn't work as long as you stay within the supported feature set. I think we have a good understanding on what the invariants are in the CoqAPI protocol, and so far there is only 1 known issue which IMO is not very important [`newtip` is not respected for certain combinations of commands inside proofs] Then of course you have bugs of the platform [Coq] itself, but now Maxime is working in trying to polish them out. Note that SerAPI does indeed try to workaround a few quirks of the STM so clients don't have to care; and it can do so with moderate success as it lives in the OCaml work. So far there has been some more serious battle testing of SerAPI by the proof engineering group, and apart from some issues with serialization the behavior seems to be pretty predictable. SerAPI is missing some critical piece of information tho: what ideal interface the Emacs people would like to have? For example, I have a branch where you can just send the full document over and over again and Coq will compute the diff and update the client about the result. [This is the seed for the LSP mode indeed] The branch is not yet public as sadly there are some platform problems that impede us to do this reliably yet, but we will get there soon I hope. As of today indeed you need to use `Add` and `Cancel` I'm much afraid. Cheers, E. ___ 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
On 29/11/2018 14.11, Emilio Jesús Gallego Arias wrote: > Clément Pit-Claudel writes: >>> Note even for the mainline, coqtop-based branch, many hacks in the code >>> could be removed today if so we wished. >> >> I'm not sure I understand this part > > See for example: > > - https://github.com/coq/coq/issues/7591 > - https://github.com/ProofGeneral/PG/issues/212 > > Among others, that would allow to drop all the code manipulating `Set > Silent`, having to parse documents, etc... Ah, yes, of course; but removing that code requires dropping support for old versions of Coq. signature.asc Description: OpenPGP digital signature ___ 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
Stefan Monnier writes: >> 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? As of today, you have coq-serapi[1], which was specifically designed to make interaction with Emacs easy. Even if I am sure the protocol would need adjustments, it already provides a way more convenient interface than the XML protocol. Also, a LSP server for Coq is expected to appear very soon. Cheers, E. [1] https://github.com/ejgallego/coq-serapi ___ 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
Clément Pit-Claudel writes: >> Note even for the mainline, coqtop-based branch, many hacks in the code >> could be removed today if so we wished. > > I'm not sure I understand this part See for example: - https://github.com/coq/coq/issues/7591 - https://github.com/ProofGeneral/PG/issues/212 Among others, that would allow to drop all the code manipulating `Set Silent`, having to parse documents, etc... Cheers, E. ___ 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
On Thu, Nov 29, 2018 at 9:35 AM Emilio Jesús Gallego Arias wrote: > 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. As the guy who wrote that branch, I tend to agree. -- Paul ___ 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
Hi Pierre, Le jeudi 29 novembre 2018 à 17:48 +0100, Pierre Courtieu a écrit : > Is a student having a 6 year old linux distrib really worth worrying? > (just kidding). For Ubuntu 14.04 I guess you just mean 4 years old (or 4.5)… as we’re still in 2018 ;) Actually what might be interesting when dealing with this kind of question is to have statistics on the emacs version used by PG users… But AFAIK this info is not provided by the MELPA repository. > Sounds good to me. OK. So to sum up, we could replace in April 2019 the requirement of emacs-24.3 with emacs-24.5, which corresponds to the latest release of the emacs package in Ubuntu xenial (16.04 LTS)… To confirm this, it seems the page https://packages.ubuntu.com/xenial/ is currently broken, but the Launchpad API is still working; cf. that oneliner inspired by https://stackoverflow.com/a/52597441/9164010: $ curl -fsSL "https://api.launchpad.net/1.0/ubuntu/+archive/primary?ws.op=getPublishedSources_name=emacs24_match=true_series=https://api.launchpad.net/1.0/ubuntu/xenial; \ | jq --raw-output ".entries | .[0] | .source_package_version" > 24.5+1-6ubuntu1.1 Kind regards, Erik -- Érik Martin-Dorel, PhD Maître de Conférences, Lab. IRIT, Univ. Toulouse 3 erik.martin-do...@irit.fr erik.martin-do...@ens-lyon.org https://www.irit.fr/~Erik.Martin-Dorel ___ 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
Le jeu. 29 nov. 2018 à 12:12, Erik Martin-Dorel a écrit : > > Hi Pierre, > > Le jeudi 29 novembre 2018 à 10:35 +0100, Pierre Courtieu a écrit : > > Do we really want to be compatible with ubuntu 14.04? I mean there are > > 18.04 and now 20.04 out there... > > Indeed it may seem quite an old release… but the EOL of Ubuntu 14.04 > will just take place in April 2019 (and I’ve seen several people still > having 14.04 on their PC, including students in my university) so we Is a student having a 6 year old linux distrib really worth worrying? (just kidding). Sounds good to me. P. > could just bump PG’s minimal required version of emacs in next April? > > Clément and Pierre, what do you think about this? ___ 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
On 29/11/2018 06.12, Erik Martin-Dorel wrote: > Clément and Pierre, what do you think about this? Sounds good to me signature.asc Description: OpenPGP digital signature ___ 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
Hi Pierre, Le jeudi 29 novembre 2018 à 10:35 +0100, Pierre Courtieu a écrit : > Do we really want to be compatible with ubuntu 14.04? I mean there are > 18.04 and now 20.04 out there... Indeed it may seem quite an old release… but the EOL of Ubuntu 14.04 will just take place in April 2019 (and I’ve seen several people still having 14.04 on their PC, including students in my university) so we could just bump PG’s minimal required version of emacs in next April? Clément and Pierre, what do you think about this? Kind regards, Erik -- Érik Martin-Dorel, PhD Maître de Conférences, Lab. IRIT, Univ. Toulouse 3 erik.martin-do...@irit.fr erik.martin-do...@ens-lyon.org https://www.irit.fr/~Erik.Martin-Dorel ___ 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
Thanks a lot Stefan, I am very worried about the async branch. Its state is not usable at this moment (lots of bugs) imho and we have nobody to maintain and fix it currently. Do we really want to be compatible with ubuntu 14.04? I mean there are 18.04 and now 20.04 out there... P. Le jeu. 29 nov. 2018 à 03:19, Stefan Monnier a écrit : > > > 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. >
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 e3daebcd..b03fedaa 100644
