| Age | Commit message (Collapse) | Author |
|---|
|
|
|
New value vos-and-vok for coq-compile-vos customization option,
existing value vos stands now for vos-no-vok. The implementation
uses the existing vio2vo infrastructure with symbols vok and
vio2vo.
Documentation is still missing.
|
|
In functions, variables and symbols vio2vo is replaced with
second-stage to accommodate for vok compilation. For backward
compatibility, the options coq-compile-vio2vo-delay and
coq-max-background-vio2vo-percentage are kept. They provide
default values for their renamed counterparts, if they have been
set manually or through the customization system.
Documentation has only been marked but not updated yet.
|
|
|
|
fixes #534
|
|
|
|
|
|
|
|
|
|
- no clones any more, existing jobs are directly linked
- the whole require command is processed by coqdep to determine
the required files, this fixes #352
- the require commands are a separate kind of jobs, because they
do not need to get compiled
- queue items are only stored in require jobs and file jobs can
not have a queue dependency, this simplifies the logic
|
|
The hash avoids an exponentially growing number of duplicates in
the ancestor collection. Fixes #499
|
|
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
|
|
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.)
|
|
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)
|
|
|
|
|
