aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
...
* | one more redundant call removedGravatar Paul Steckler2017-03-06
| |
* | remove redundant calls, simplify codeGravatar Paul Steckler2017-03-06
| |
* | Merge pull request #163 from ProofGeneral/fix_indentationGravatar Pierre Courtieu2017-03-03
|\ \ | | | | | | Fix indentation
* | | Refreshing goal when Set Printing xxx. (#162)Gravatar Pierre Courtieu2017-03-03
| | | | | | | | | | | | | | | * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open).
* | | use Utf8 from Coq libraryGravatar Paul Steckler2017-03-02
| | |
* | | serveral coqtags fixes and improvementsGravatar Hendrik Tews2017-02-27
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* | | Fixing #154.Gravatar Pierre Courtieu2017-02-23
| |/ |/|
| * Fixing #147 and #91 + others indentation bugs.Gravatar Pierre Courtieu2017-01-26
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | While fixing these I discovered several flaws in indentation (what a suprise). The probem is the following: since we don't have a precise grammar of tactics, smie often decides that the parent of a sub-part of a tactic is the previous command instead of the current tacic. Typical example (fixed now but in general): foo. apply bar with bar'. Since "apply ... bar'" is considered as one leaf of the grammar, it is considered to be a child of the previous dot. . /\ / \ foo apply...bar' Therefore indentation of "with" wants to align with parent "." and hence with "foo". Basically we should try to define a much more precise grammar of complex tactics (with with, as, using etc) in order to fix the problem. Of course this has the drawback of making impossible to support user tactic notations.
* save settings not defined with defpacustom (fixes #142)Gravatar Hendrik Tews2017-01-19
| | | | | | | - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
* split emergency-cleanup to handle interrupts properly (fixes #143)Gravatar Hendrik Tews2017-01-18
| | | | | | Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
* fix coqtagsGravatar Hendrik Tews2017-01-17
| | | | @psteckler I believe you have this patch already in your branch.
* Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106)Gravatar Jason Gross2017-01-17
|
* Merge pull request #107 from JasonGross/patch-3Gravatar hendriktews2017-01-17
|\ | | | | Add Context to coq-syntax.el
* | Fix prooftree for Coq 8.6Gravatar Hendrik Tews2017-01-14
| | | | | | | | | | | | | | 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.
* | add second argument to looking-back, required in emacs25Gravatar Hendrik Tews2016-12-31
| |
* | properly reset the vio2vo delay timerGravatar Hendrik Tews2016-12-28
| | | | | | | | | | cancel-timer does of course not set the variable that holds the timer to nil
* | Merge pull request #133 from hendriktews/file-errorGravatar hendriktews2016-12-16
|\ \ | | | | | | die gracefully when visiting files in nonexisting directories
* | | add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Gravatar Hendrik Tews2016-12-15
| | |
* | | fix :get for coq-search-blacklistGravatar Hendrik Tews2016-12-15
| | |
* | | Merge pull request #101 from tchajed/print-universes-optionGravatar hendriktews2016-12-15
|\ \ \ | | | | | | | | Add Set Printing Universes to options menu
| | * | die gracefully when visiting files in nonexisting directoriesGravatar Hendrik Tews2016-12-15
| |/ / |/| |
* | | fix generic interrupt procedure to interrupt parallel background compilationGravatar Hendrik Tews2016-12-14
| | |
* | | fix race in vio2vo compilation startGravatar Hendrik Tews2016-12-14
| | |
* | | Merge pull request #129 from hendriktews/keep-goingGravatar hendriktews2016-12-14
|\ \ \ | | | | | | | | Keep going
* \ \ \ Merge pull request #132 from Matafou/masterGravatar Pierre Courtieu2016-12-14
|\ \ \ \ | | | | | | | | | | Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
| * | | | Same name guessing for coqc/coqdep then for coqtop.Gravatar Pierre Courtieu2016-12-13
| | | | |
| * | | | remove default absolute name from coq-prog-name, but keep dipsplaying it ↵Gravatar Pierre Courtieu2016-12-12
| | | | | | | | | | | | | | | | | | | | when asking for it.
| | * | | documentation and CHANGES for coq-compile-keep-goingGravatar Hendrik Tews2016-12-08
| | | | |
| | * | | option coq-compile-keep-going for parallel compilationGravatar Hendrik Tews2016-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
| | * | | remove ancestor hash in Coq parallel background compilationGravatar Hendrik Tews2016-12-02
| |/ / / |/| | |
* | | | fix customize-group coqGravatar Hendrik Tews2016-11-30
| | | |
* | | | style change: use when for if coq-debug-auto-compilationGravatar Hendrik Tews2016-11-30
| | | |
* | | | use coq-- for internal compilation variablesGravatar Hendrik Tews2016-11-30
| | | |
* | | | next-error support for vio2vo error messagesGravatar Hendrik Tews2016-11-30
| | | |
* | | | update documentationGravatar Hendrik Tews2016-11-29
| | | |
* | | | delay vio2vo compilationGravatar Hendrik Tews2016-11-29
| | | | | | | | | | | | | | | | | | | | ... to make it less likely people run into the library inconsistency issue with vio2vo
* | | | 8.4 compatibility for quick supportGravatar Hendrik Tews2016-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | don't unnecessarily delete .vio files for ensure-voGravatar Hendrik Tews2016-11-29
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | support vio2vo background processingGravatar Hendrik Tews2016-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | | improve compilation when both .vio and .vo are up-to-dateGravatar Hendrik Tews2016-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | reconcile menu for auto compilationGravatar Hendrik Tews2016-11-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | fix parallel compilation for the unlikely case of identical time stampsGravatar Hendrik Tews2016-11-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | first version for quick compilationGravatar Hendrik Tews2016-11-16
|/ / / | | | | | | | | | | | | | | | Select "Quick compilation mode" in the Coq menu. See also documentation of coq-compile-quick, the and-vio2vo stuff is not yet there.
* | | avoid leaving partial files behind when compilation failsGravatar Hendrik Tews2016-11-10
| | |
* | | fix #123, also improve debugging outputGravatar Hendrik Tews2016-11-02
| | |
* | | ensure coq-compile-response-buffer is not in a dedicated windowGravatar Hendrik Tews2016-10-28
| | | | | | | | | | | | This makes #54 a bit less critical.
* | | fix coq-require-command-regexp (fixes #75)Gravatar Hendrik Tews2016-10-28
| | |
* | | fix typo in last commitGravatar Hendrik Tews2016-10-28
| | |
* | | give a more helpful error message if Coq version detection failsGravatar Hendrik Tews2016-10-27
| | | | | | | | | | | | | | | | | | | | | - coq--pre-v85 signals coq-unclassifiable-version for "Invalid version" errors - background compilation converts this into an even more helpful message (fixes #70)
* | | fix parallel compilation and improve assertions and debugging codeGravatar Hendrik Tews2016-10-27
| | | | | | | | | | | | - fixes #92
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:27:34 +0000