aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Gaëtan Gilbert2018-01-11
| | | | | | PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1
* Merge PR #6234: Make the micromega extraction check a regular output test.Gravatar Maxime Dénès2017-12-20
|\
* | Circle CI: cat failed test suite logsGravatar Gaëtan Gilbert2017-12-14
| |
| * Make the micromega extraction check a regular output test.Gravatar Gaëtan Gilbert2017-11-28
|/ | | | | This allows us to enforce that it works without breaking the build when it doesn't.
* Universe binders survive sections, modules and compilation.Gravatar Gaëtan Gilbert2017-11-25
|
* Merge PR #6123: Nix fileGravatar Maxime Dénès2017-11-23
|\
* | Fixing encoding in coqdoc output tests.Gravatar Hugo Herbelin2017-11-13
| | | | | | | | | | | | | | | | | | | | The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
| * Introduce default.nix for Nix users.Gravatar Théo Zimmermann2017-11-09
|/ | | | | This file can be used to get in an environment ready to compile Coq (with `nix-shell`) or to compile and install Coq (with `nix-build`).
* add coqwc testsGravatar Paul Steckler2017-10-03
|
* Avoid running interactive tests on Windows.Gravatar Maxime Dénès2017-08-29
| | | | | This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests.
* Fix coqdoc test-suite target on Windows.Gravatar Théo Zimmermann2017-08-21
| | | | | | Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite.
* Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Gravatar Maxime Dénès2017-08-16
|\ | | | | | | wrongly tagged as keywords
* | fake_ide: do as coqide to find out coqtop pathGravatar Enrico Tassi2017-07-20
| |
* | Remove trailing CR before diff in output and misc tests.Gravatar Maxime Dénès2017-07-20
| |
* | Print failure logs on appveyor.Gravatar Maxime Dénès2017-07-20
| |
* | Make coqlib relative in test suite (revert 024a7ab20b0)Gravatar Maxime Dénès2017-07-20
| |
| * Adding a coqdoc target to test-suite.Gravatar Hugo Herbelin2017-07-17
|/ | | | | | | One file was already ready for testing. We add another one. Note that we have to remove the machine-dependent lines in the output tex files.
* Fix Travis sectioningGravatar Jason Gross2017-06-10
| | | | | | | It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right?
* Better sectioning on travis log printing in test-suiteGravatar Jason Gross2017-06-09
|
* Merge PR#711: [gitlab] Artifact test suite logs on failure.Gravatar Maxime Dénès2017-06-02
|\
* \ Merge PR#704: Fix empty parentheses display in test-suiteGravatar Maxime Dénès2017-06-01
|\ \
| | * [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | |
| * | Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was an extra trailing space in #680. Now things display as, e.g., ``` TEST bugs/opened/3754.v TEST bugs/opened/4803.v (-compat 8.4) ``` instead of ``` TEST bugs/opened/3754.v ( ) TEST bugs/opened/4803.v (-compat 8.4 ) ```
* / [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
|/ | | | We only want an absolute path, no need to follow symlinks.
* Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\
| * Gitlab CIGravatar Gaëtan Gilbert2017-05-28
| |
* | add Show test with -emacs flagGravatar Paul Steckler2017-05-25
|/
* test suite for coq_makefile2Gravatar Enrico Tassi2017-05-23
|
* test suite for coq_makefileGravatar Enrico Tassi2017-05-23
|
* Re-adding explicit dependency of misc universe test into all_stdlib.v.Gravatar Hugo Herbelin2017-05-19
| | | | | | | Was working when calling test-suite from main Makefile but not when calling directly from the test-suite Makefile. The dependency was mistakenly dropped in 98a927aef.
* Moving code for miscellaneous tests to specific files.Gravatar Hugo Herbelin2017-05-10
| | | | | | | | | | | | | | | | | | The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
* A more regular naming of variables in test-suite Makefile.Gravatar Hugo Herbelin2017-05-10
|
* Adding tests for testing exit status and #use"include".Gravatar Hugo Herbelin2017-05-10
|
* Rename lia.cache into .lia.cache in the test-suite Makefile.Gravatar Maxime Dénès2016-10-24
|
* Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
| | | | + a few improvements on 5f1dd4c40 (lexing of { and }).
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\
| * Adding dependency of the test-suite subsystems in prerequisite (fixing #5150).Gravatar Hugo Herbelin2016-10-20
| |
* | test-suite/output-modulo-time made more robustGravatar Enrico Tassi2016-09-30
| | | | | | | | Order of items made stable
* | Merge remote-tracking branch 'github/pr/303' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ | | | | | | | | | Was PR#303: LtacProf cutoff is for total percent, not time
* \ \ Merge remote-tracking branch 'github/pr/302' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ | | | | | | | | | | | | Was PR#302: Set the default LtacProf cutoff to 2%
* | | | 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
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 02:18:14 +0000