| Age | Commit message (Collapse) | Author |
|---|
|
faces: Extend highlights to EOL to adjust for latest Emacs changes
|
|
|
|
Generic monadic indentation + specifically ext-lib / Compcert + doc.
|
|
This a generalization of PR#451 proposed by @Chobbes.
Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.
NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".
NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.
|
|
|
|
Recognize "Timeout" before save keywords to fix #446
|
|
viz. '("Defined" "Save" "Qed" "End" "Admitted" "Abort" "Proof")
|
|
Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444
|
|
|
|
Make -topfile facility work for unnamed files
|
|
|
|
coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility
|
|
Use coqc for vio2vo compilation instead of coqtop for
Coq >= 8.10+alpha.
With https://github.com/coq/coq/pull/8690 vio2vo
compilation (-schedule-vio2vo) was moved from coqtop to coqc, see
also https://github.com/coq/coq/issues/10679. This commit makes
PG compilation compatible with Coq after that PR. However, the
patch only checks for the Coq version, therefore making PG vio2vo
compilation fail on 8.10 versions before PR 8690. (Compilation
still works, it's just that vio2vo postprocessing for the mode
quick-and-vio2vo fails.)
|
|
Backtrack -> BackTo
|
|
|
|
Coq script example to reproduce:
--8<---------------cut here---------------start------------->8---
Set Nested Proofs Allowed.
Lemma foo : True /\ 1 = 1.
split. (*2*)
easy.
Goal True /\ 2 = 2. (*1-bug*)
Proof. (*1-ok*)
split; easy.
Qed.
easy.
Qed.
--8<---------------cut here---------------end--------------->8---
1. goto-point (*1-bug*) (just before the comment)
2. goto-point (*2*) (bug: the goal is not shown)
3. goto-point (*1-ok*) (just after "Proof.")
4. goto-point (*2*) (no bug)
|
|
href: coq/coq#10574
* Define a variable coq--retract-naborts to handle the communication
of [coq-find-and-forget -> coq-empty-action-list-command] that used
to be done through the third argument of Backtrack.
* Refactor coq-empty-action-list-command, replacing the occurrences of
string-match with string-match-p.
|
|
fix coqtags that can't find some theorem and output empty definition
|
|
|
|
Due to performance issue (probably an emacs bug) and given the
uselessness of the pghelp spans in retracted regions. We simply remove
these spans when retracting.
The question remains to remove them completely or to make them more
useful. company-coq currently disables them anyway.
|
|
|
|
Proof diffs revisions requested by @monnier
|
|
|
|
|
|
Remove stray h
|
|
Fixes #424
|
|
(coq-insert-with-face): Don't assume we're at EOB.
* generic/pg-goals.el (pg-goals-display): Use with-current-buffer.
* generic/pg-response.el (pg-response-maybe-erase): Narrow the scope of
inhibit-read-only.
(pg-response-display-with-face): Use `member`. Remove unused var `end`.
Only bind `start` when we have a value for it.
(proof-trace-buffer-display): Use with-current-buffer.
|
|
Support Coq's proof diffs feature: highlight diffs in goals and some error messages
|
|
FIX #422.
|
|
the output of coqtop-help is now stored in a variable like coq's version.
|
|
context (with diff annotations when enabled).
|
|
This bug seems to date from the generalization performed in commit:
080babbb0f361885e9b502ee56dec14351104a37
|
|
This patch allows one to load the `coq-diffs' option at Coq startup,
provided the ambient Coq version is >= 8.10.
This additional "lambda" format is needed because [Set Diffs "on".] is neither:
- a boolean setting from Coq side (there are three possible values)
- a string setting from Emacs side (it is implemented as a radio/symbol option)
- a cross-version compatible Coq setting.
|
|
using Coq's proof diffs feature.
|
|
|
|
Clean -topfile for coq-prog-args properly
|
|
This makes it possible to run new and old coq versions consecutively
without manually cleaning coq-prog-args.
|
|
Derive proof-mode from prog-mode
|
|
prog-mode [1] is the base mode for programming that comes with Emacs:
“All major modes for programming languages should derive from this mode
so that users can put generic customization on prog-mode-hook.” Make
proof-mode derive from prog-mode, reflecting its status as a programming
mode.
[1] https://git.savannah.gnu.org/cgit/emacs.git/tree/lisp/progmodes/prog-mode.el?id=a18336a8dc754fa1c68e16dd8009466cf409271b
|
|
|
|
Stefan's cleanup stumbled on my lack of comments :-(. Some function
was supposed to return point found if found.
|
|
Revert proof-general.el to 05df29f7ff065d8da45b81691c602b6cf075e4a0/pg-init.el
(modulo comments).
|
|
The previous code raised some bytecomp errors when loading a ~/.emacs
containing a bootstrapped use-package proof-general config., such as:
```
(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
(not (gnutls-available-p))))
(proto (if no-ssl "http" "https")))
(add-to-list 'package-archives
(cons "melpa" (concat proto "://melpa.org/packages/")) t))
(package-initialize)
;; Bootstrap use-package
(unless (package-installed-p 'use-package)
(package-refresh-contents)
(package-install 'use-package))
(eval-when-compile
(require 'use-package))
(use-package proof-general
:ensure t
:mode ("\\.v\\'" . coq-mode))
```
|
|
Improve use-package support
|
|
as this text should document the whole package and will be shown at
http://www.melpa.org/#/proof-general
href: https://github.com/ProofGeneral/PG/issues/198#issuecomment-419741803
|
|
as PG master is still under GPLv2 (while PG async already switched to GPLv3+)
href: https://github.com/ProofGeneral/PG/tree/fb3b75dab55b6e6befffc53e136422558be5faa0#contributing
|
|
Close ProofGeneral/PG#385 and close ProofGeneral/PG#398
|
|
* generic/pg-user.el (proof-add-completions): `proof-assistant` can
also be the empty string :-(
|
|
Revise the various `require`s to avoid spurious dependencies, and tweak
the code here and there to eliminate the remaining dependencies.
* coq/coq-db.el: Don't require proof-config nor proof-syntax.
(coq-build-opt-regexp-from-db): Avoid proof-regexp-alt-list.
* coq/coq-indent.el: Use lexical-binding. Don't require coq-syntax.
Comment out all the code that's not used any more.
(coq-empty-command-p): Use forward-comment instead of
coq-find-not-in-comment-backward. Fix paren typos.
(coq-script-parse-cmdend-forward, coq-script-parse-cmdend-backward):
Use forward-comment i.s.o proof-script-generic-parse-find-comment-end.
Use syntax-ppss i.s.o proof-buffer-syntactic-context.
(coq-find-current-start): Explicit case-fold-search i.s.o proof-looking-at.
* coq/coq-mode.el (coq-mode): Set comment-start/end.
* coq/coq-smie.el: Require coq-syntax explicitly.
(coq-smie-detect-goal-command, coq-smie-module-deambiguate):
Explicit case-fold-search i.s.o proof-looking-at.
(coq-indent-basic): New custom var.
(coq-smie-rules): Use it in case PG is not loaded.
* coq/coq-syntax.el: Don't require proof-syntax, proof-utils, and span.
(coq-goal-command-p): Use overlay-get i.s.o span-property.
(coq-save-command-regexp-strict, coq-save-command-regexp):
Use \` and regexp-opt i.s.o proof-anchor-regexp and proof-ids-to-regexp.
(coq-save-command-p): Explicit case-fold-search i.s.o proof-string-match.
(coq--regexp-alt-list-symb): Rename from proof-regexp-alt-list-symb.
Use mapconcat i.s.o proof-regexp-alt-list.
(coq-save-with-hole-regexp): Use regexp-opt i.s.o proof-regexp-alt-list.
(coq-goal-command-regexp, coq-goal-with-hole-regexp)
(coq-decl-with-hole-regexp, coq-defn-with-hole-regexp)
(coq-font-lock-keywords-1): Use mapconcat i.s.o proof-regexp-alt-list.
(coq-find-first-hyp, coq-detect-hyps-positions-in-goals):
Use current buffer i.s.o proof-goals-buffer.
(coq-with-altered-syntax-table): Fix broken use of unwind-protect.
* coq/coq.el (coq-detect-hyps-in-goals): Change buffer before calling
coq-find-first-hyp and coq-detect-hyps-positions-in-goals.
(coq-pg-setup): Use comment-start/end.
* generic/pg-goals.el: Require proof-script explicitly instead of
autoloading via proof-insert-sendback-command.
* generic/pg-pbrpm.el: Require proof-script explicitly instead of
autoloading via proof-insert-pbp-command.
* generic/pg-pgip.el: Require proof-script explicitly.
* generic/proof-depends.el: Require proof-script explicitly instead of
autoloading via pg-set-span-helphighlights.
* generic/proof-script.el (pg-set-span-helphighlights)
(proof-insert-pbp-command, proof-insert-sendback-command)
(proof-script-generic-parse-find-comment-end): Don't autoload.
* generic/proof-syntax.el (proof-ids-to-regexp): Simplify.
* lib/span.el (span-delete): η-reduce.
|
|
* generic/proof-autoloads.el: Remove `require`s; not needed.
* generic/proof-site.el: Don't require `pg-vars`.
(proof-ready-for-assistant): Move to proof-script.el.
* generic/proof-menu.el (proof-assistant-format): Make dynamically
scoped var explicit (preparation for lexical-binding).
* generic/proof-script.el: Require `pg-vars`.
(proof-ready-for-assistant): Move from proof-site.el.
* generic/proof-syntax.el (proof-replace-regexp-in-string):
* generic/proof-shell.el (proof-shell-live-buffer): Don't mark it
as inlinable: it's not performance sensitive.
|
