| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
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.
|
|
This hopefully fixes compilation without coqtop and especially
the github tests.
|
|
Use process-file and omit find-file-name-handler, because
process-file takes care of file handlers already.
Fixes #525
|
|
This commit adds support for the new -vos compilation. For coq >=
8.11 only -vos can be used, depending on the config option
coq-compile-vos. For coq < 8.11 only -quick/-vio is used,
depending on option coq-compile-quick, as before. For a smooth
upgrade path, if coq-compile-vos has not been configured, the
users intention on whether to use -vos or not for coq >= 8.11 is
derived from coq-compile-quick.
Some defaults have been changed:
- parallel background compilation is the default now in case
coq-compile-before-require is enabled.
- for coq < 8.11, quick/vio compilation with delayed vio-to-vo
conversion is now the default
|
|
|
|
|
|
For the record:
- "-topfile" option is good so that coqtop understands the name of the
current module
- but some people want to script coq files with incorrect names
without ever comiling them. So we don't add "-topfile" option when it
would make coqtop fail. A warning is issued.
|
|
|
|
the output of coqtop-help is now stored in a variable like coq's version.
|
|
This makes it possible to run new and old coq versions consecutively
without manually cleaning coq-prog-args.
|
|
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.
|
|
This fix is not completely satisfying for the following reason:
1- I had to add a new hook in generic code. But I don't see how we
could avoid this: the computation of options must happen AFTER the
proof-prog-name is asked to the user, because this computation
depends on the version of coq.
2- We should fix the synchronization between coq-prog-name and
proof-prog-name. Either remove coq-prog-name and use only
proof-prog-name, or have the generic coq always point to
some (proof-ass-sym prog-name).
|
|
|
|
|
|
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.
|
|
When editing a remote file, the `coqtop` process will itself be remote, which
means that the paths that are passed to it should be _local_, not remote.
Otherwise, paths like '/ssh:hostname:/path/to/dir' get passed to `coqtop`, which
has no idea what's going on.
This relates to #203.
|
|
The result of parsing was in reverse, see
https://github.com/ProofGeneral/PG/issues/392\#issuecomment-425227314
|
|
|
|
|
|
By renaming the arg load-path into loadpath I notice that a
coq-load-path was used instead of it.
|
|
Make coq-prog-args safe when list of strings.
|
|
|
|
|
|
They could be passed through _CoqProject regardless.
|
|
|
|
This fixes a bunch of compilation warnings
|
|
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
|
|
It didn't really matter that these variables were defined and set to nil during
compilation, since we ran compilation in a clean Emacs in --batch mode; it does
matter now, however, since package.el compiles PG in the user's currently
running Emacs instance.
|
|
While fixing these I discovered several flaws in indentation (what a
suprise). The probem is the following: since we don't have a precise
grammar of tactics, smie often decides that the parent of a sub-part
of a tactic is the previous command instead of the current tacic.
Typical example (fixed now but in general):
foo.
apply bar
with bar'.
Since "apply ... bar'" is considered as one leaf of the grammar, it is
considered to be a child of the previous dot.
.
/\
/ \
foo apply...bar'
Therefore indentation of "with" wants to align with parent "." and
hence with "foo".
Basically we should try to define a much more precise grammar of
complex tactics (with with, as, using etc) in order to fix the
problem. Of course this has the drawback of making impossible to
support user tactic notations.
|
|
In Coq 8.6 evar status printing is off by default, causing
prooftree to crash. This patch inserts invisible commands to
switch evar status printing on and off. This is done via the
urgent-action-hook.
|
|
|
|
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
|
|
|
|
when asking for it.
|
|
|
|
- coq--pre-v85 signals coq-unclassifiable-version for "Invalid
version" errors
- background compilation converts this into an even more helpful
message (fixes #70)
|
|
- fixes #92
|
|
|
|
Rationale: if Coq isn't installed, we will detect it when trying to run
it, and we don't need to duplicate the error logic.
Additionally, change from using process-lines to using shell-command,
possibly through file-name-handler. The reason for this change is that
we want to do the version detection on the remote server if we're
running in Tramp.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
