| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
... 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.
|
|
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.
|
|
Making coq-compile-quick configurable via the Settings menu would
require a lot of work, because the
defpacustom/proof-menu-define-settings-menu engine does only work
for simple types. On second sight, I believe the Settings menu
and the whole engine behind it are more intended for options that
configure the proof assistant behind Proof General. Taking this
together, I believe, it makes more sense to have a separate menu
entry for auto compilation in the Coq menu. This submenu contains
all the options for background compilation. The compilation
entries from the settings menu should be deleted, probably after
the next release.
|
|
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.
|
|
|
|
|
|
- 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
|
|
|
|
This addresses part of the issues pointed out in #112
|
|
|
|
|
|
|
|
Closes #99.
|
|
|
|
This may look ugly to the majority, so I let it off by default.
I find it helpfull to have structuring symbols bold.
|
|
Closes #81
|
|
|
|
|
|
|
|
|
|
|
|
This closes #77
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
Quote at start of a word should not be considered part of the word.
Other characters than ' or _ are punctuation.
|
|
It's too recent
|
|
Fixes #67.
|
|
|
|
|
|
|
|
There are many other issued with coq-smie-forward-token.
|
|
More robust to font-lock tweaks that change font inside
comments (whitespace mode etc).
|
