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
>> 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
> 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 decla
f-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=UT
> 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
> 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 warn
> 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
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
> 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
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
> 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
> 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.
s 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
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
> 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
> 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
>> 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
(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
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
- 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,
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
21 matches
Mail list logo
