| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-22 | Fix #7704: get_toplevel_path needs normalised argv.(0) | Gaëtan Gilbert | |
| When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways. | |||
| 2018-06-04 | test suite: make target to regenerate failing output tests | Gaëtan Gilbert | |
| 2018-05-25 | Allow make clean to work on a fresh clone | Jason Gross | |
| The file `config/Makefile` doesn't exist unless we run `./configure`. We shouldn't have to run `./configure` to run `make clean`. We now no longer error in any case if `config/Makefile` doesn't exist; this is simpler than only not erroring if the target is `clean`. We also now test this property when building on CI. This fixes #7542 | |||
| 2018-05-16 | Modify make system to include Makefile.common in the test suite | Gaëtan Gilbert | |
| 2018-05-16 | add unit tests to test suite | Paul Steckler | |
| 2018-05-15 | [ssr] import ssreflect test suite from math-comp | Enrico Tassi | |
| 2018-04-22 | test suite: clean more things (glob, MExtraction.out, distclean aux) | Gaëtan Gilbert | |
| NB: I made .aux be cleaned only with distclean imitating the main Makefile. | |||
| 2018-04-22 | test suite: print message for failing tests as they come | Gaëtan Gilbert | |
| ie you might see make TEST bugs/closed/1337.v TEST bugs/closed/3263.v TEST bugs/closed/7777.v FAILED bugs/closed/3263.v.log TEST bugs/opened/1.v ... report: 3263 failed (should be closed) | |||
| 2018-04-22 | test suite Makefile: do not use %.stamp for subsystem targets | Gaëtan Gilbert | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-01-11 | Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | Gaëtan Gilbert | |
| PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1 | |||
| 2017-12-20 | Merge PR #6234: Make the micromega extraction check a regular output test. | Maxime Dénès | |
| 2017-12-14 | Circle CI: cat failed test suite logs | Gaëtan Gilbert | |
| 2017-11-28 | Make the micromega extraction check a regular output test. | Gaëtan Gilbert | |
| This allows us to enforce that it works without breaking the build when it doesn't. | |||
| 2017-11-25 | Universe binders survive sections, modules and compilation. | Gaëtan Gilbert | |
| 2017-11-23 | Merge PR #6123: Nix file | Maxime Dénès | |
| 2017-11-13 | Fixing encoding in coqdoc output tests. | Hugo Herbelin | |
| 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. | |||
| 2017-11-09 | Introduce default.nix for Nix users. | Théo Zimmermann | |
| 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`). | |||
| 2017-10-03 | add coqwc tests | Paul Steckler | |
| 2017-08-29 | Avoid running interactive tests on Windows. | Maxime Dénès | |
| This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests. | |||
| 2017-08-21 | Fix coqdoc test-suite target on Windows. | Théo Zimmermann | |
| 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. | |||
| 2017-08-16 | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵ | Maxime Dénès | |
| wrongly tagged as keywords | |||
| 2017-07-20 | fake_ide: do as coqide to find out coqtop path | Enrico Tassi | |
| 2017-07-20 | Remove trailing CR before diff in output and misc tests. | Maxime Dénès | |
| 2017-07-20 | Print failure logs on appveyor. | Maxime Dénès | |
| 2017-07-20 | Make coqlib relative in test suite (revert 024a7ab20b0) | Maxime Dénès | |
| 2017-07-17 | Adding a coqdoc target to test-suite. | Hugo Herbelin | |
| 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. | |||
| 2017-06-10 | Fix Travis sectioning | Jason Gross | |
| 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? | |||
| 2017-06-09 | Better sectioning on travis log printing in test-suite | Jason Gross | |
| 2017-06-02 | Merge PR#711: [gitlab] Artifact test suite logs on failure. | Maxime Dénès | |
| 2017-06-01 | Merge PR#704: Fix empty parentheses display in test-suite | Maxime Dénès | |
| 2017-05-31 | [travis] print failing test suite logs on failure | Gaëtan Gilbert | |
| 2017-05-30 | Fix empty parentheses display in test-suite | Jason Gross | |
| 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 ) ``` | |||
| 2017-05-30 | [readlink -f] doesn't work on OSX | Gaëtan Gilbert | |
| We only want an absolute path, no need to follow symlinks. | |||
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès | |
| 2017-05-28 | Gitlab CI | Gaëtan Gilbert | |
| 2017-05-25 | add Show test with -emacs flag | Paul Steckler | |
| 2017-05-23 | test suite for coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | test suite for coq_makefile | Enrico Tassi | |
| 2017-05-19 | Re-adding explicit dependency of misc universe test into all_stdlib.v. | Hugo Herbelin | |
| 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. | |||
| 2017-05-10 | Moving code for miscellaneous tests to specific files. | Hugo Herbelin | |
| 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. | |||
| 2017-05-10 | A more regular naming of variables in test-suite Makefile. | Hugo Herbelin | |
| 2017-05-10 | Adding tests for testing exit status and #use"include". | Hugo Herbelin | |
| 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% | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |