aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
Commit message (Collapse)AuthorAge
...
* | | | Restore code ignoring <W> lines in output (camlp5 warnings)Gravatar Enrico Tassi2016-09-30
| | | |
* | | | Ignore file names in warning emitted by test-suite/output/* (#5111)Gravatar Enrico Tassi2016-09-30
| | | |
| | * | LtacProf cutoff is for total percent, not timeGravatar Jason Gross2016-09-29
| |/ / |/| |
| * | Set the default LtacProf cutoff to 2%Gravatar Jason Gross2016-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 +Gravatar Matthieu Sozeau2016-09-29
| |
* | test-suite/output-modulo-time made more robustGravatar Enrico Tassi2016-09-13
| |
* | Add support for testing output mod timing changesGravatar Jason Gross2016-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 4836Gravatar Jason Gross2016-09-11
| | | | | | | | | | This required improving the machinery of the test-suite Makefile to support -compile.
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\|
| * test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
| |
* | fix test-suite/ide Makefile (stupid typo)Gravatar Enrico Tassi2016-06-15
| |
* | test-suiet: run fake_id as before pr/173 was mergedGravatar Enrico Tassi2016-06-14
| |
* | STM: code cleanupGravatar Enrico Tassi2016-05-10
| |
* | Do that "make" in test-suite writes failures as a default togetherGravatar Hugo Herbelin2016-04-19
| | | | | | | | with a more explicit message.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
| |
* | New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
|/
* Univs: the stdlib now needs 5 universesGravatar Matthieu Sozeau2015-10-02
| | | | Prop < Set < i for every global univ i
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
|
* test-suite: Fix test-suite MakefileGravatar Matthieu Sozeau2015-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-suiteGravatar Enrico Tassi2015-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/* testsGravatar Enrico Tassi2015-03-30
|
* There was one more universe needed due to the use of now ↵Gravatar Matthieu Sozeau2015-01-18
| | | | | | non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again.
* Back to 4 expected universes.Gravatar Matthieu Sozeau2015-01-17
|
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* include test-suite/coqchk in the summary logGravatar Enrico Tassi2014-12-27
|
* new test for coqchkGravatar Enrico Tassi2014-12-26
|
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
|
* typoGravatar Enrico Tassi2014-12-10
|
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
|
* Fix test flags for fake_ideGravatar Enrico Tassi2014-11-27
|
* Use return code to classify anomalies as active open bugs.Gravatar Xavier Clerc2014-11-14
|
* Classify segfaults as failures in opened bugs.Gravatar Xavier Clerc2014-10-03
|
* Classify segfaults as failures in opened bugsGravatar Xavier Clerc2014-10-03
|
* Added make dependency in %.out in output tests.Gravatar Hugo Herbelin2014-10-02
|
* Updating to the new use of 3 universes, after Hurkens is simplified.Gravatar Hugo Herbelin2014-10-01
|
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
|
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* fixup fakeide test-suiteGravatar Pierre Boutillier2014-07-24
|
* Update test-suite Makefile to handle coq-prog-argsGravatar Jason Gross2014-05-02
|
* Adapt test-suite to -I is ML onlyGravatar Pierre Boutillier2014-04-09
|
* Remove option -g as it is non-portable yet does not have any effect on the ↵Gravatar Guillaume Melquiond2014-04-04
| | | | test-suite. (Fix for bug #3024)
* fake_ide: ported to spawnGravatar Enrico Tassi2014-02-10
|
* Testsuite: flatten the 'bugs/opened' directory.Gravatar xclerc2013-11-29
|
* Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)Gravatar xclerc2013-11-28
|
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 23:14:22 +0000