| Age | Commit message (Collapse) | Author |
|---|
|
Add feature to omit complete opaque proofs
|
|
|
|
|
|
|
|
Work around the wrong order returned by `overlays-at' in
Emacs <= 25.
|
|
|
|
|
|
Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.
|
|
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.
With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.
To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
|
|
|
|
|
|
|
|
Actually it seems that even multimatch and lazymatch was poorly
supported.
|
|
Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.
To squash.
|
|
Closes GH-557.
|
|
There's no need for ("not" . ?¬) because Coq already has a "~" for it.
|
|
test: Add Emacs 27.1 in CI & Bump the minimal-required version of Emacs (24.5 for now)
|
|
feat: Add proof-upgrade-menu triggering proof-upgrade-elpa-packages
|
|
* Lastly, package-menu-async keeps its initial value even if we C-g.
|
|
|
|
|
|
|
|
protect uses of coq-callcoq
|
|
* require package.el (in a safe way thanks to `proof-try-require`)
|
|
* Document (in README.md) the proposed policy: supporting Emacsen from
the versions packaged in Debian Stable / Ubuntu LTS until their EOS.
|
|
Uses of coq-callcoq need to correctly handle nil as result for
the case that coq-callcoq fails.
Additionally, add a regression test.
Fixes #551
|
|
Fix a tiny typo
|
|
|
|
|
|
|
|
New value vos-and-vok for coq-compile-vos customization option,
existing value vos stands now for vos-no-vok. The implementation
uses the existing vio2vo infrastructure with symbols vok and
vio2vo.
Documentation is still missing.
|
|
In functions, variables and symbols vio2vo is replaced with
second-stage to accommodate for vok compilation. For backward
compatibility, the options coq-compile-vio2vo-delay and
coq-max-background-vio2vo-percentage are kept. They provide
default values for their renamed counterparts, if they have been
set manually or through the customization system.
Documentation has only been marked but not updated yet.
|
|
This action checks that
- make -C doc magic works
- the manual is currently up-to-date
The second check fails when somebody changes variable or function
documentation of something that appears in one of the manuals
without updating the manuals at the same time. Further, it fails
when emacs changes such that the function `texi-docstring-magic'
produces different output.
|
|
|
|
Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.
|
|
Switching to lexical scope and emacs using closure (instead of
lambda) broke argument printing with make magic.
|
|
Set text quoting style to get doc strings without unicode single
quotation marks to keep the regular expressions in
texi-docstring-magic working.
|
|
In 7389d43893569ff0e1eff892254901876fc8225e
proof-ready-for-assistant was moved to proof-script.el, breaking
make magic in a complicated chain. The auto load for
proof-ready-for-assistant caused proof-script.el to be loaded
before proof-assistant was set, causing
proof-eval-when-ready-for-assistant, to put stuff into
proof-ready-for-assistant-hook. proof-ready-for-assistant loads
pg-custom.el by require, therefore, for the first proof assistant
in the loop in docstring-magic everything was defined when
executing the hooks at the end of proof-ready-for-assistant. The
second assistant caused errors than.
Fixes #542
|
|
this problem was introduced in a921439a4eb5b0d96182748e779c78e2f6a41a5f
|
|
After 574b09 92e3cb4b7a4ad88400b9a5ab0198a96ca5, make magic fails
with a recursive require chain. No requires were changed in that
commit, it's unclear to me, why there is no recursive require
chain with (eval-when (compile).
|
|
Coq team is currently considering changing all messages containing
"subgoal[s]" into "goal[s]". This commit allows for both.
I make this change as early as possible, even if this chage may not
land in coq's master, so that we support this as early as possible.
I don't see how this could break anything but again the earliest the
best.
|
|
|
|
fixes #534
|
|
|
|
|
|
|
|
extend the github workflow to additionally run the tests in
ci/compile-tests
|
|
|
|
See also the committed test.el. The test is not completely
robust, it needs to be improved in the future.
|
|
|
