[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[NonGNU ELPA] Proof-General version 4.5
From: |
ELPA update |
Subject: |
[NonGNU ELPA] Proof-General version 4.5 |
Date: |
Wed, 13 Jul 2022 17:03:09 -0400 |
Version 4.5 of package Proof-General has just been released in NonGNU ELPA.
You can now find it in M-x package-list RET.
Proof-General describes itself as:
A generic Emacs interface for proof assistants
More at https://elpa.nongnu.org/nongnu/proof-general.html
Recent NEWS:
-*- outline -*-
This is a summary of main changes. For details, please see
the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
* Changes of Proof General 4.5 from Proof General 4.4
** Generic changes
*** License changed to GPLv3+
*** Remove support for the following systems:
Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.
*** require GNU Emacs 25.2 or later
The current policy aims at supporting multiple Emacs versions,
including those available in distributions Debian Stable
(https://packages.debian.org/stable/emacs) and Ubuntu LTS
(https://packages.ubuntu.com/emacs), until their End-Of-Support (see
also https://wiki.ubuntu.com/Releases). Support for Emacs 25 will
be dropped in April 2023 when Ubuntu Bionic reaches end of
standard support.
*** new command and menu item to easily upgrade all packages
- To upgrade all ELPA packages (including ProofGeneral if it was
installed via MELPA), do "M-x proof-upgrade-elpa-packages RET"
or use the "Proof-General > Upgrade ELPA packages..." menu item
*** bug fixes
- Using query-replace (or replace-string) in the processed region
doesn't wrongly jump to the first match anymore.
- cheat face (admit etc) now visible when locked.
*** remove key-binding for proof-electric-terminator-toggle
- The default key-binding for proof-electric-terminator-toggle
(C-c .) was too easy to enter by mistake. And it was not that
useful as we can expect users to configure electric-terminator
once and for all. Hence the removal of this default key-binding.
*** add another (fallback) key-binding for proof-goto-point
- The default key-binding for proof-goto-point (C-c <C-return>)
was not available in TTYs. Now, this function can also be run
with "C-c RET", which happens to be automatically trigerred if
we type "C-c <C-return>" in a TTY.
*** new proof-priority-action-list
Similar to proof-action-list, but holding actions that need
to go to the proof assistant at the next opportunity.
** Qrhl-tool
Support for qrhl-tool theorem prover has been added by Dominique
Unruh.
References:
- Initial pull request: https://github.com/ProofGeneral/PG/pull/636
- Qrhl-tool web site: https://dominique-unruh.github.io/qrhl-tool
** EasyCrypt
Support for EasyCrypt has been added.
** Coq changes
*** fix highlighting issues for ssr tactics ending with colon
Now, { exact: term. } will always be correctly highlighted.
However, only (forall {T: Type}, Type) will be highlighted,
unlike term (forall { T: Type }, Type) that has a spurious space.
Also in (forall [T: Type], Type), variable T is now highlighted.
*** new menu Coq -> Auto Compilation for all background compilation options
*** support for 8.11 vos and vok compilation
See menu Coq -> Auto Compilation -> vos compilation, option
coq-compile-vos and subsection "11.3.3 Quick and inconsistent
compilation" in the Coq reference manual.
*** support for 8.5 quick compilation
See new menu Coq -> Auto Compilation -> Quick compilation.
Select "no quick" as long as you have not switched to "Proof
using" to compile without -quick. Select "quick no vio2vo" to
use -quick without vio2vo (and guess what "quick and vio2vo"
means ;-), select "ensure vo" to ensure a sound development.
Quick compilation is only supported for Coq < 8.11. See the
option `coq-compile-quick' or the subsection "11.3.3 Quick
and inconsistent compilation" in the Coq reference manual.
*** new option coq-compile-keep-going (in menu Coq -> Auto Compilation)
Similar to ``make -k'', with this option enabled, background
compilation does not stop at the first error but rather
continues as far as possible.
*** Automatic insertion of "Proof using" annotations.
PG now supports the "Suggest Proof Using" by inserting
(automatically or by contextual menu or by a command) the "Proof
using" annotation suggested by Coq. This suggestion happens at
...
...
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [NonGNU ELPA] Proof-General version 4.5,
ELPA update <=