| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Closes GH-557.
|
|
proof-state-change-pre-hook happens earlier than
proof-state-change-hook, i.e. before proof-done-advancing. This should
be used to register information in the currently processed span before
proof-done-advancing classifies it.
Historically PG design was to gather these information during
proof-done-advancing (or in its hook called at the end) by just
looking at the command statement. But it is often useful to look at
the output (messages and/or prompt) to gather more accurate
information. Some of this information may be needed DURING
proof-done-advancing. Hence this early hook.
|
|
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.
|
|
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
|
|
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.
|
|
Move the part of coq.el that is not specific to ProofGeneral into coq-mode.el
to make `coq-mode` into a major mode that can work without PG.
* coq/coq-mode.el: New file, with code extracted from coq.el.
(coq-use-pg): New var.
(coq-near-comment-region): Complete rewrite.
* Makefile.devel (autoloads): Add `coq` to the scanned subdirectories.
* generic/proof-autoloads.el: Regenerate.
* generic/proof-site.el: Don't override pre-existing major-mode definitions.
* coq/coq-syntax.el (coq-init-syntax-table): Delete function.
Setup the syntax-table while loading coq-mode.el instead.
* coq/coq-system.el (coq-prog-name, get-coq-library-directory)
(coq-library-directory, coq-tags): Move to coq-mode.el.
* coq/coq.el: Set proof-assistant when loaded.
(coq-may-use-prettify, coq-outline-regexp)
(coq-outline-heading-end-regexp, coq-mode)
(coq-prettify-symbols-alist, coq-fill-paragraph-function)
(coq-adaptive-fill-function): Move to coq-mode.el.
(coq-shell-mode-syntax-table, coq-response-mode-syntax-table)
(coq-goals-mode-syntax-table): Just reuse the already setup
coq-mode-syntax-table...
(coq-shell-mode-config, coq-goals-mode-config, coq-response-config):
... instead of calling coq-init-syntax-table.
(coq-get-comment-region): Delete, not used any more.
(coq-pg-mode-map): New var. Move top-level keymap setup here.
(coq-pg-setup): Rename from coq-mode-config.
Move all the non-PG specific settings to coq-mode.
* generic/proof-script.el (proof-mode): Simplify call to
proof-splash-message since it does the same extra tests internally.
(proof-config-done-related): Don't touch font-lock-defaults if the mode
doesn't provide any font-lock-defaults.
* isar/isar-syntax.el: Use lexical-binding.
(isar-font-lock-fontify-syntactically-region): Make it
callable from font0lock-keywords.
(isar-font-lock-keywords-1):
Call isar-font-lock-fontify-syntactically-region.
* generic/proof-syntax.el (font-lock-fontify-keywords-region):
Remove advice.
(proof-ids): Remove, unused.
* lib/bufhist.el (bufhist-erase-buffer):
Don't let-bind after-change-functions.
* generic/pg-pbrpm.el (pg-pbrpm-auto-select-around-point):
Fix one more left-over cl.el use.
* generic/proof-utils.el (proof-with-script-buffer): Add edebug spec.
|
|
Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f),
so loading a file should "no effect". Fix the most obvious such effects:
the splash screen and the autotests by moving those effects into a function.
* coq/coq-autotest.el: Make it declarative. Use lexical-binding.
(coq-autotest): New function holding the code that used to be at top-level.
* generic/proof.el: Use lexical-binding.
Don't call proof-splash-message just because we're being loaded.
* generic/proof-script.el: Use lexical-scoping; fix all warnings.
(pg-show-all-portions): Simplify the code with a closure.
(proof-activate-scripting): Declare activated-interactively as dyn-scoped.
(proof--splash-done): New var.
(proof-mode): Call proof-splash-message upon first use.
* generic/proof-splash.el (proof-splash-message): Don't check
byte-compile-current-file now that we're only called when the mode
is activated.
* acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'.
* coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²).
* coq/coq-seq-compile.el:
* coq/coq-par-test.el:
* coq/coq-par-compile.el: Fix leftover uses of CL's `assert`.
* generic/proof-utils.el:
* generic/pg-movie.el:
* etc/testsuite/pg-test.el:
* coq/coq-syntax.el: Fix leftover uses of CL's `incf`.
* generic/pg-autotest.el: Fix leftover uses of CL's `decf`.
* obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use
of CL's `loop`.
* generic/pg-user.el (proof-add-completions): Do nothing if no
proof-assistant is set yet (i.e. during byte-compilation).
(byte-compile-current-file): No need to test this any more.
* generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat.
Remove unnecessary "\\(?:...\\)".
(proof-regexp-alt): Redefine in terms of proof-regexp-alt-list.
|
|
Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.
* coq/coq-db.el: Use lexical-binding.
* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.
* coq/coq.el: Require `span` to silence some warnings.
* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.
* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.
* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.
* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!
* lib/holes.el: Use lexical-binding.
Remove redundant :group args.
* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.
|
|
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&restores
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.
|
|
Fix #158 by extending helpspan
|
|
|
|
|
|
This commit address ProofGeneral/PG#193.
|
|
|
|
Close ProofGeneral/PG#160
|
|
|
|
Fixes #65
|
|
proof-script-buffer was not set before calling proof-shell-ready-prover.
|
|
|
|
This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).
|
|
|
|
|
|
|
|
* generic/proof-site.el (assistants): Fix regexp.
|
|
comment-start-skip: if it is already set then proof-script should not
change it. Ultimately if David approves we should moreover fix the
setting itself which is bugged.
coq-mode now sets this variable by itself.
|
|
interactive-p with called-interactively-p)
|
|
|
|
coq-compile-response-buffer
- fix typo elsewhere
|
|
avoid hitting read only error in calling command.
|
|
|
|
removing restriction during automatic retraction so
proof-retract-until-point behaves correctly.
|
|
|
|
proof-last-edited-low-watermark.
|
|
http://proofgeneral.inf.ed.ac.uk/trac/ticket/395
|
|
proof-shell-require-command-regexp
- TAGS updated to really flush them
|
|
|
|
who read or edit by waving mouse at text
|
|
- improve internal docs for unlocking
|
|
|
|
intelligible, also to properly support behaviour needed for
`proof-no-fully-processed-buffer'.
|
|
now a list of functions to be run when the span is deleted. Use
span-add-delete-action to add a delete action.
|
|
Addresses Trac #383
|
|
|
|
- add documentation for it
- add a test case demonstrating it in
coq/ex/test-cases/retract-completely-asserted
|
|
The following points are implemented already:
- recompile either via an external command (make) or let
ProofGeneral handle everything internally
- complete dependency tracking and recompilation for coq files in
internal mode
- support for extending the LoadPath: does almost work, even if
specified file-locally
- move back to clean state if recompilation fails
There are the following known problems:
- coq-load-path extensions are not retracted
- fails on partially qualified library names
|
|
|
|
|
