| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-24 | Rename lia.cache into .lia.cache in the test-suite Makefile. | Maxime Dénès | |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Hugo Herbelin | |
| + a few improvements on 5f1dd4c40 (lexing of { and }). | |||
| 2016-10-21 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
| 2016-10-20 | Adding dependency of the test-suite subsystems in prerequisite (fixing #5150). | Hugo Herbelin | |
| 2016-09-30 | test-suite/output-modulo-time made more robust | Enrico Tassi | |
| Order of items made stable | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/303' into v8.6 | Maxime Dénès | |
| Was PR#303: LtacProf cutoff is for total percent, not time | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/302' into v8.6 | Maxime Dénès | |
| Was PR#302: Set the default LtacProf cutoff to 2% | |||
| 2016-09-30 | Restore code ignoring <W> lines in output (camlp5 warnings) | Enrico Tassi | |
| 2016-09-30 | Ignore file names in warning emitted by test-suite/output/* (#5111) | Enrico Tassi | |
| 2016-09-29 | LtacProf cutoff is for total percent, not time | Jason Gross | |
| 2016-09-29 | Set the default LtacProf cutoff to 2% | Jason Gross | |
| 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. | |||
| 2016-09-29 | test-suite: fix sed on OS X, does not handle + | Matthieu Sozeau | |
| 2016-09-13 | test-suite/output-modulo-time made more robust | Enrico Tassi | |
| 2016-09-11 | Add support for testing output mod timing changes | Jason Gross | |
| 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. | |||
| 2016-09-11 | Add a test for 4836 | Jason Gross | |
| This required improving the machinery of the test-suite Makefile to support -compile. | |||
| 2016-07-04 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2016-07-04 | test-suite: test checking of libraries checksum. | Maxime Dénès | |
| 2016-06-15 | fix test-suite/ide Makefile (stupid typo) | Enrico Tassi | |
| 2016-06-14 | test-suiet: run fake_id as before pr/173 was merged | Enrico Tassi | |
| 2016-05-10 | STM: code cleanup | Enrico Tassi | |
| 2016-04-19 | Do that "make" in test-suite writes failures as a default together | Hugo Herbelin | |
| with a more explicit message. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Adding a target report to test-suite's Makefile to get a short summary. | Hugo Herbelin | |
| 2015-12-01 | New algorithm for universe cycle detections. | Jacques-Henri Jourdan | |
| 2015-10-02 | Univs: the stdlib now needs 5 universes | Matthieu Sozeau | |
| Prop < Set < i for every global univ i | |||
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-07-07 | test-suite: Fix test-suite Makefile | Matthieu Sozeau | |
| Using relative path for coqlib, for some reason this fails on Mac OS X. Took the easiest way to fix it. | |||
| 2015-05-29 | Flag -test-mode intended to be used for ad-hoc prints in test-suite | Enrico Tassi | |
| 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. | |||
| 2015-03-30 | camlp4: grep away warnings in output/* tests | Enrico Tassi | |
| 2015-01-18 | There was one more universe needed due to the use of now ↵ | Matthieu Sozeau | |
| non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again. | |||
| 2015-01-17 | Back to 4 expected universes. | Matthieu Sozeau | |
| 2015-01-09 | STM: fix handling of side effects in vio2vo | Enrico Tassi | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2014-12-27 | include test-suite/coqchk in the summary log | Enrico Tassi | |
| 2014-12-26 | new test for coqchk | Enrico Tassi | |
| 2014-12-11 | Test suite: keep message in sync with actual file deletions. | Xavier Clerc | |
| 2014-12-10 | typo | Enrico Tassi | |
| 2014-12-10 | test-suite: few tests for ".v -> .vi -> .vo" compilation chain | Enrico Tassi | |
| 2014-11-27 | Fix test flags for fake_ide | Enrico Tassi | |
| 2014-11-14 | Use return code to classify anomalies as active open bugs. | Xavier Clerc | |
| 2014-10-03 | Classify segfaults as failures in opened bugs. | Xavier Clerc | |
| 2014-10-03 | Classify segfaults as failures in opened bugs | Xavier Clerc | |
| 2014-10-02 | Added make dependency in %.out in output tests. | Hugo Herbelin | |
| 2014-10-01 | Updating to the new use of 3 universes, after Hurkens is simplified. | Hugo Herbelin | |
| 2014-09-18 | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier | |
| 2014-09-16 | Undo prints only if coqtop || emacs | Enrico Tassi | |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot | |
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |