| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- precise tags for definitions
- fix bug with nonempty white space lines
- add several keywords (Proposition, Record, ...)
- generate tags for constructors of inductive definitions
and for record labels
|
|
|
|
- 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.
|
|
@psteckler I believe you have this patch already in your branch.
|
|
|
|
Add Context to coq-syntax.el
|
|
In Coq 8.6 evar status printing is off by default, causing
prooftree to crash. This patch inserts invisible commands to
switch evar status printing on and off. This is done via the
urgent-action-hook.
|
|
|
|
cancel-timer does of course not set the variable that holds the
timer to nil
|
|
die gracefully when visiting files in nonexisting directories
|
|
|
|
|
|
Add Set Printing Universes to options menu
|
|
|
|
|
|
|
|
Keep going
|
|
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
|
|
|
|
when asking for it.
|
|
|
|
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.
|
|
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
|
|
|
|
|
|
|
