aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
AgeCommit message (Collapse)Author
2018-09-13Move test suite report script to standalone script fileGaëtan Gilbert
This allows for nicer formatting without having to deal with Make's semantic whitespace.
2018-09-12Merge PR #8243: Remove xargs from "make clean" so it won't fail on CygwinEnrico Tassi
2018-09-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
This fixes the fix 1522b989 to #7192. The remaining Not_found after 1522b989 should have rung a bell that something was still strange.
2018-08-30Replace use of xargs in "make clean", which tends to fail on Windows/Cygwin.Jim Fehrle
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
GitLab setup is quite stable these days thanks to the work of many people and `coqbot`. We decided to keep CircleCI support for a while as a safeguard in case something happened in the migration to GitLab, but these days we are just wasting resources to them and to us. As I'm afraid CircleCI won't scale for us, the time to remove it has arrived. Still, CircleCI had some awesome functionality that GitLab's CI doesn't offer yet, see the links at: https://github.com/coq/coq/issues/6919#issuecomment-395885573 - https://gitlab.com/gitlab-org/gitlab-ce/issues/29347 - https://gitlab.com/gitlab-org/gitlab-ce/issues/35222 - https://gitlab.com/gitlab-org/gitlab-ce/issues/41947 - https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
2018-06-22Fix #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-04test suite: make target to regenerate failing output testsGaëtan Gilbert
2018-05-25Allow make clean to work on a fresh cloneJason 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-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16add unit tests to test suitePaul Steckler
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-04-22test 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-22test suite: print message for failing tests as they comeGaë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-22test suite Makefile: do not use %.stamp for subsystem targetsGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-11Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGaëtan Gilbert
PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1
2017-12-20Merge PR #6234: Make the micromega extraction check a regular output test.Maxime Dénès
2017-12-14Circle CI: cat failed test suite logsGaëtan Gilbert
2017-11-28Make 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-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-23Merge PR #6123: Nix fileMaxime Dénès
2017-11-13Fixing 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-09Introduce 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-03add coqwc testsPaul Steckler
2017-08-29Avoid 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-21Fix 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-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Maxime Dénès
wrongly tagged as keywords
2017-07-20fake_ide: do as coqide to find out coqtop pathEnrico Tassi
2017-07-20Remove trailing CR before diff in output and misc tests.Maxime Dénès
2017-07-20Print failure logs on appveyor.Maxime Dénès
2017-07-20Make coqlib relative in test suite (revert 024a7ab20b0)Maxime Dénès
2017-07-17Adding 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-10Fix Travis sectioningJason 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-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-02Merge PR#711: [gitlab] Artifact test suite logs on failure.Maxime Dénès
2017-06-01Merge PR#704: Fix empty parentheses display in test-suiteMaxime Dénès
2017-05-31[travis] print failing test suite logs on failureGaëtan Gilbert
2017-05-30Fix empty parentheses display in test-suiteJason 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 OSXGaëtan Gilbert
We only want an absolute path, no need to follow symlinks.
2017-05-29Merge PR#687: Gitlab CIMaxime Dénès
2017-05-28Gitlab CIGaëtan Gilbert
2017-05-25add Show test with -emacs flagPaul Steckler
2017-05-23test suite for coq_makefile2Enrico Tassi
2017-05-23test suite for coq_makefileEnrico Tassi
2017-05-19Re-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-10Moving 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-10A more regular naming of variables in test-suite Makefile.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2016-10-24Rename lia.cache into .lia.cache in the test-suite Makefile.Maxime Dénès
2016-10-24Merge branch 'v8.5' into v8.6Hugo Herbelin
+ a few improvements on 5f1dd4c40 (lexing of { and }).
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 21:01:36 +0000