| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
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
|