| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
This fixes a bunch of compilation warnings
|
| |
|
|
|
|
| |
This file is `require'-d from other places, at compile time. This doesn't work
nicely with compilation by package.el (PG complains and says "defpacustom: Proof
assistant setting compile-before-require re-defined!")
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
Split coq-par-emergency-cleanup into two functions, one for
reacting on user interrupts and one for cleaning up after
compilation errors.
|
| |
|
|
|
| |
cancel-timer does of course not set the variable that holds the
timer to nil
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
With this option set, compilation continues after the first error
to compile as much as possible and to potentially report more
than one error.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
... to make it less likely people run into the library
inconsistency issue with vio2vo
|
| |
|
|
|
|
| |
If both .vio and .vo exists, coq loads the newer one. Therefore,
for ensure-vo, don't delete up-to-date .vio files when the .vo is
newer.
|
| |
|
|
|
|
|
|
|
|
|
| |
Selecting quick-and-vio2vo will start vio2vo conversion in the
background on a subset of the available cores, see
`coq-max-background-vio2vo-percentage'. The vio2vo conversion
starts after all compilation for the require command has been
finished and the require has been processed. Because of a certain
incompatibility between .vio and .vo files (see coq issue 5223)
slowly single stepping through require commands does not
work (but processing them as a batch does).
|
| |
|
|
|
|
|
|
|
|
|
|
| |
In this case Coq loads the younger file and emits a warning if
the .vio file is the younger one. With this patch, the dependency
analysis for parallel compilation continues with the older value.
The interesting case to look at is when b.v depends on a.v and
both are compiled with -quick and later a parallel vio2vo
produces a.vo and b.vo such that b.vo is older (because, eg. b.v
is shorter than a.v). Without this patch a second auto
compilation would recompile b.v, because the dependency a.vo is
younger.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Since version 24.3 Emacs supports pico second precision in time
stamps and Emacs on ext4 seems to have a time precision of 5
milliseconds for file time stamps. It is therefor quite unlikely
that a source and an object file have the same time stamp. This
patch fixes parallel compilation for these corner cases and adds
a few hundred test cases to test all combinations where some
files have identical time stamps. On Emacs older than 24.3 or on
file systems with a low precision (eg. ext3) this patch can cause
additional compilations.
|
| |
|
|
|
|
| |
Select "Quick compilation mode" in the Coq menu. See also
documentation of coq-compile-quick, the and-vio2vo stuff is not yet
there.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
- 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
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Need some more refactoring actually: Some code from coq-compile-common
became necessary to coq/pg globally. We shoudl refelct this by moving
these parts somewhere else.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Bug recipe:
* Process some imports
* Enable on the fly compilation
* Kill coq process
Error:
Debugger entered--Lisp error: (wrong-type-argument hash-table-p nil)
maphash((lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files)))) nil)
(progn (maphash (function (lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files))))) coq-par-ancestor-files))
(if (or t coq-par-ancestor-files) (progn (maphash (function (lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files))))) coq-par-ancestor-files)))
coq-par-unlock-ancestors-on-error()
coq-par-emergency-cleanup()
run-hooks(proof-shell-signal-interrupt-hook)
proof-shell-kill-function()
kill-buffer(#<buffer *coq*>)
proof-shell-exit(nil)
funcall-interactively(proof-shell-exit nil)
#<subr call-interactively>(proof-shell-exit nil nil)
ad-Advice-call-interactively(#<subr call-interactively> proof-shell-exit nil nil)
apply(ad-Advice-call-interactively #<subr call-interactively> (proof-shell-exit nil nil))
call-interactively(proof-shell-exit nil nil)
command-execute(proof-shell-exit)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
- fix aborting background compilation on error
|
| |
|
|
| |
- better handling of errors in process creation
|
| | |
|
| | |
|
| | |
|
|
|
coq-par-compile.el (must be activated via
coq-compile-parallel-in-background)
- items in the queue region are not necessarily in
proof-action-list any more! Require commands and the following
items are stored elsewhere until the compilation finishes.
Variable proof-second-action-list-active notifies the generic
machinery if queue items are stored elsewhere. In this case,
Proof General must neither release the proof shell lock nor
delete the queue span when proof-action-list is empty.
- to kill background processes as early as possible, the new hook
proof-shell-signal-interrupt-hook is used
|
Stefan Monnier
Erik Martin-Dorel
Clément Pit--Claudel
Hendrik Tews
Pierre Courtieu