aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
AgeCommit message (Expand)Author
2021-04-23test-suite: add approve-coqdoc to update all coqdoc output files at once.Hugo Herbelin
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2020-11-20Merge PR #13248: Build all_stdlib.v in test suite makefilecoqbot-app[bot]
2020-11-20[CI] Deactivate native-compiler for a few tests that fail with itPierre Roux
2020-11-20Build all_stdlib.v in test suite makefileGaëtan Gilbert
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its documenta...Hugo Herbelin
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-19Improve `make approve-output`Jason Gross
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the tes...Martin Bodin
2020-08-19No more arithmetic directory test-suite.Hugo Herbelin
2020-08-18Change OUnit package name to ounit2.Tanaka Akira
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-05-22[coqchk] Add testPierre Roux
2020-05-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
2020-05-18Merge PR #12289: test-suite: fix bug causing unit tests to be skippedHugo Herbelin
2020-05-18[test-suite] Ensure copies of files are writableEmilio Jesus Gallego Arias
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-17Revert "[test] unit tests for ide/coq_lex.ml" + makefile supportGaëtan Gilbert
2020-05-17test-suite: fix bug causing unit tests to be skippedGaëtan Gilbert
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
2020-04-12Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.Hugo Herbelin
2020-04-12[test-suite] Remove deprecated -I option of coqchk in MakefilePierre Roux
2020-03-26Fix calling test suite makefile with a dune built coqGaëtan Gilbert
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-16Fix coq-makefile/native1 testPierre Roux
2020-02-28Makefile in test-suite: More separation of concerns as suggested by Enrico.Hugo Herbelin
2020-02-28Fixed some escaping problems with arguments containing spaces in IDE's Compil...Ike Mulder
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-04Fixing status reporting for complexity tests.Hugo Herbelin
2019-12-19Remove trailing \r in complexity measures for WindowsJason Gross
2019-12-19Better error reporting when res is not what is expectedJason Gross
2019-12-19Fix complexity test-suite failure reporting on WinJason Gross
2019-12-19Revert "Fix #11303: skip complexity tests on windows even if bogomips found"Jason Gross
2019-12-19Fix #11303: skip complexity tests on windows even if bogomips foundGaëtan Gilbert
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-11-27Display more information when complexity tests failJason Gross
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Implementing support for vos/vok files.charguer
2019-11-01Add tests for primitive floatsGuillaume Bertholon
2019-10-14test-suite/Makefile: work when manually involved for dune-compiled CoqGaëtan Gilbert
2019-06-25Merge PR #10412: Add output-coqtop test directory that runs output tests with...Enrico Tassi
2019-06-24Merge PR #10394: [ide] chop sentences taking into account QUOTATION tokenPierre-Marie Pédrot
2019-06-20Add output-coqtop test directory that runs output tests with coqtopJim Fehrle