aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-30fix customize-group coqHendrik Tews
2016-11-30fix 2 compilation warnings (fixes #33)Hendrik Tews
2016-11-30style change: use when for if coq-debug-auto-compilationHendrik Tews
2016-11-30Merge pull request #125 from hendriktews/quickhendriktews
support for quick compilation
2016-11-30use coq-- for internal compilation variablesHendrik Tews
2016-11-30write CHANGESHendrik Tews
2016-11-30next-error support for vio2vo error messagesHendrik Tews
2016-11-29update documentationHendrik Tews
2016-11-29delay vio2vo compilationHendrik Tews
... to make it less likely people run into the library inconsistency issue with vio2vo
2016-11-298.4 compatibility for quick supportHendrik Tews
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.
2016-11-29don't unnecessarily delete .vio files for ensure-voHendrik Tews
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.
2016-11-29support vio2vo background processingHendrik Tews
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).
2016-11-22improve compilation when both .vio and .vo are up-to-dateHendrik Tews
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.
2016-11-18reconcile menu for auto compilationHendrik Tews
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.
2016-11-17fix parallel compilation for the unlikely case of identical time stampsHendrik Tews
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.
2016-11-16first version for quick compilationHendrik Tews
Select "Quick compilation mode" in the Coq menu. See also documentation of coq-compile-quick, the and-vio2vo stuff is not yet there.
2016-11-10avoid leaving partial files behind when compilation failsHendrik Tews
2016-11-02fix #123, also improve debugging outputHendrik Tews
2016-11-02fix error in process filter: Cannot resize windowHendrik Tews
2016-10-28ensure coq-compile-response-buffer is not in a dedicated windowHendrik Tews
This makes #54 a bit less critical.
2016-10-28fix coq-require-command-regexp (fixes #75)Hendrik Tews
2016-10-28fix typo in last commitHendrik Tews
2016-10-27Merge pull request #118 from hendriktews/several-fixeshendriktews
I believe this PR will also fix #119, therefore I think it is good to merge it now.
2016-10-27give a more helpful error message if Coq version detection failsHendrik Tews
- coq--pre-v85 signals coq-unclassifiable-version for "Invalid version" errors - background compilation converts this into an even more helpful message (fixes #70)
2016-10-27gitignore for doc subdirHendrik Tews
2016-10-27delete TAGS file from repositoryHendrik Tews
2016-10-27fix parallel compilation and improve assertions and debugging codeHendrik Tews
- fixes #92
2016-10-16Update CHANGES.Erik Martin-Dorel
Related: ProofGeneral/PG#41
2016-10-15Follow-up of #115.Erik Martin-Dorel
2016-10-14Merge pull request #115 from tchajed/macos-rebrandingErik Martin-Dorel
Refer to Apple's operating system as macOS
2016-10-14Refer to Apple's operating system as macOSTej Chajed
Starting with the latest version (10.12 "Sierra"), the operating system is called macOS rather than Mac OS X.
2016-09-28Makefile: don't depend on pwdClément Pit--Claudel
2016-09-28Make it possible to work around #113Clément Pit--Claudel
2016-09-25proof-retract-before-change: Fix #41 by saving/restoring the match data.Erik Martin-Dorel
2016-09-24Update .travis.yml.Erik Martin-Dorel
2016-09-23Disable parallel build, to workaround the issue raised in PR #112.Erik Martin-Dorel
2016-09-19Make shell and perl scripts executable.Erik Martin-Dorel
This addresses part of the issues pointed out in #112
2016-09-19Bump version number for next release cycle.Erik Martin-Dorel
2016-09-18Update the documentation and prepare the release 4.4.Erik Martin-Dorel
2016-09-18Comment-out the rcsid ($Id$) that dates from CVS.Erik Martin-Dorel
2016-09-18Detail.Erik Martin-Dorel
2016-09-18Promote CHANGES since 2820cb68 as related to PG 4.4.Erik Martin-Dorel
2016-09-16Fix reference to log-warning-minimum-levelpsteckler
Fixes #110.
2016-09-01Add Context to coq-syntax.elJason Gross
2016-08-25Ensure PG overlays have pg-span property (#98)Tej Chajed
2016-08-15Add Set Printing Universes to options menuTej Chajed
2016-08-14Sort the OPTIONS menu items differently & Fix a typo (UnSet -> Unset).Erik Martin-Dorel
2016-08-14Replace "Set Implicit Arguments" option with "Set Printing Implicit".Erik Martin-Dorel
Closes #99.
2016-08-14Add Reserved Infix like Reserved Notation (#95)Jason Gross
2016-07-26Fix whitespace to comply with Markdown syntax.Erik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:38:58 +0000