Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | test-suite/output-modulo-time made more robust | 2016-09-30 | |
| | | | | Order of items made stable | ||
* | Merge remote-tracking branch 'github/pr/303' into v8.6 | 2016-09-30 | |
|\ | | | | | | | Was PR#303: LtacProf cutoff is for total percent, not time | ||
* \ | Merge remote-tracking branch 'github/pr/302' into v8.6 | 2016-09-30 | |
|\ \ | | | | | | | | | | Was PR#302: Set the default LtacProf cutoff to 2% | ||
* | | | Restore code ignoring <W> lines in output (camlp5 warnings) | 2016-09-30 | |
| | | | |||
* | | | Ignore file names in warning emitted by test-suite/output/* (#5111) | 2016-09-30 | |
| | | | |||
| | * | LtacProf cutoff is for total percent, not time | 2016-09-29 | |
| |/ |/| | |||
| * | Set the default LtacProf cutoff to 2% | 2016-09-29 | |
|/ | | | | | | | | | | | This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time. | ||
* | test-suite: fix sed on OS X, does not handle + | 2016-09-29 | |
| | |||
* | test-suite/output-modulo-time made more robust | 2016-09-13 | |
| | |||
* | Add support for testing output mod timing changes | 2016-09-11 | |
| | | | | | | | | Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table. | ||
* | Add a test for 4836 | 2016-09-11 | |
| | | | | | This required improving the machinery of the test-suite Makefile to support -compile. | ||
* | Merge branch 'v8.5' into trunk | 2016-07-04 | |
|\ | |||
| * | test-suite: test checking of libraries checksum. | 2016-07-04 | |
| | | |||
* | | fix test-suite/ide Makefile (stupid typo) | 2016-06-15 | |
| | | |||
* | | test-suiet: run fake_id as before pr/173 was merged | 2016-06-14 | |
| | | |||
* | | STM: code cleanup | 2016-05-10 | |
| | | |||
* | | Do that "make" in test-suite writes failures as a default together | 2016-04-19 | |
| | | | | | | | | with a more explicit message. | ||
* | | Merge branch 'v8.5' | 2015-12-08 | |
|\| | |||
| * | Fix some typos. | 2015-12-07 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-12-03 | |
|\| | |||
| * | Adding a target report to test-suite's Makefile to get a short summary. | 2015-12-02 | |
| | | |||
* | | New algorithm for universe cycle detections. | 2015-12-01 | |
|/ | |||
* | Univs: the stdlib now needs 5 universes | 2015-10-02 | |
| | | | | Prop < Set < i for every global univ i | ||
* | Updating the documentation and the toolchain w.r.t. the change in -compile. | 2015-09-25 | |
| | |||
* | test-suite: Fix test-suite Makefile | 2015-07-07 | |
| | | | | | Using relative path for coqlib, for some reason this fails on Mac OS X. Took the easiest way to fix it. | ||
* | Flag -test-mode intended to be used for ad-hoc prints in test-suite | 2015-05-29 | |
| | | | | | | | Of course there is an exception to the previous commit. Fail used to print even if silenced but loading a vernac file. This behavior is useful only in tests, hence this flag. | ||
* | camlp4: grep away warnings in output/* tests | 2015-03-30 | |
| | |||
* | There was one more universe needed due to the use of now ↵ | 2015-01-18 | |
| | | | | | | non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again. | ||
* | Back to 4 expected universes. | 2015-01-17 | |
| | |||
* | STM: fix handling of side effects in vio2vo | 2015-01-09 | |
| | |||
* | rename: vi -> vio | 2015-01-06 | |
| | |||
* | include test-suite/coqchk in the summary log | 2014-12-27 | |
| | |||
* | new test for coqchk | 2014-12-26 | |
| | |||
* | Test suite: keep message in sync with actual file deletions. | 2014-12-11 | |
| | |||
* | typo | 2014-12-10 | |
| | |||
* | test-suite: few tests for ".v -> .vi -> .vo" compilation chain | 2014-12-10 | |
| | |||
* | Fix test flags for fake_ide | 2014-11-27 | |
| | |||
* | Use return code to classify anomalies as active open bugs. | 2014-11-14 | |
| | |||
* | Classify segfaults as failures in opened bugs. | 2014-10-03 | |
| | |||
* | Classify segfaults as failures in opened bugs | 2014-10-03 | |
| | |||
* | Added make dependency in %.out in output tests. | 2014-10-02 | |
| | |||
* | Updating to the new use of 3 universes, after Hurkens is simplified. | 2014-10-01 | |
| | |||
* | Reductionops: (Co)Fixpoints are always refolded during iota | 2014-09-18 | |
| | |||
* | Undo prints only if coqtop || emacs | 2014-09-16 | |
| | |||
* | Removing dead code relative to the XML plugin. | 2014-09-08 | |
| | |||
* | fixup fakeide test-suite | 2014-07-24 | |
| | |||
* | Update test-suite Makefile to handle coq-prog-args | 2014-05-02 | |
| | |||
* | Adapt test-suite to -I is ML only | 2014-04-09 | |
| | |||
* | Remove option -g as it is non-portable yet does not have any effect on the ↵ | 2014-04-04 | |
| | | | | test-suite. (Fix for bug #3024) | ||
* | fake_ide: ported to spawn | 2014-02-10 | |
| |