| 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.
|
|
|
|
- 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
|
|
|
|
|
|
|
|
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 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 helps with, for example, org-src-fontification buffers.
https://lists.gnu.org/archive/html/emacs-orgmode/2016-03/msg00354.html
|
|
|
|
|
|
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!")
|
|
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.
|
|
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
Split coq-par-emergency-cleanup into two functions, one for
reacting on user interrupts and one for cleaning up after
compilation errors.
|
|
|
|
|
|
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
|
|
8.4 compatibility is done by ignoring all quick settings for
`coq-compile-quick' via a :set function. This does only work if
this variable is only changed via the customization system and
not directly via setq.
|
|
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.
|
|
This makes #54 a bit less critical.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
Command line options changed heavily betwenn 8.4 and 8.5. We need an
option to force V8.4 in some cases, mainly to infer the right
coqtop/coqdep invocations.
|
|
This comes from Hendrik's compile mode and is actually needed even
when this mode is off. When switching scripting buffer, restart the
coq shell process, so that it applies local coqtop options.
|
|
the emacs bug seems solved: the error with read-only always occur
whatever locale is used. So I toggle read-only off in
coq-compile-response.
|
|
|
|
|
|
- fix aborting background compilation on error
|
|
|
|
|
|
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
|
|
|
