aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile
Commit message (Collapse)AuthorAge
* Convert timing tools to run with both python2 and python3Gravatar Jasper Hugunin2018-07-04
|
* [ci] Fix another issue with the timing testsGravatar Jason Gross2018-04-26
| | | | | There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure.
* Improve shell scriptsGravatar zapashcanon2018-04-05
|
* Update coq_makefile timing testGravatar Jason Gross2018-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes #5675 (in yet another way). The issue was that `$` (end of string regex) was not properly escaped in `"`s. This handles the issue that is displayed in ``` cat A.v.timing.diff After | Code | Before || Change | % Change --------------------------------------------------------------------------------------------------- 0m01.44s | Total | 0m01.56s || -0m00.12s | -7.92% --------------------------------------------------------------------------------------------------- 0m00.609s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.627s || -0m00.01s | -2.87% 0m00.527s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.552s || -0m00.02s | -4.52% 0m00.304s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.379s || -0m00.07s | -19.78% N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.006s || -0m00.00s | -100.00% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A --- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000 +++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000 @@ -1,4 +1,4 @@ - N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | N/A + N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | -% ------ ------ After | Code | Before || Change | % Change ``` where, because `Declare Reduction` takes 0.006s rather than 0s, the % change shows up as -100% rather than N/A.
* Merge PR #6756: Fix issue with spurious timing test failuresGravatar Maxime Dénès2018-02-28
|\
| * [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
| | | | | | | | As per https://github.com/coq/coq/pull/6756/files#r168028764
* | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \
| * | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| | |
| * | also test vio2voGravatar Ralf Jung2018-02-15
| | |
| * | test "make quick2vo"Gravatar Ralf Jung2018-02-15
| | |
* | | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
|/ / | | | | | | | | | | | | | | This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it.
| * Fix issue with spurious timing test failuresGravatar Jason Gross2018-02-13
|/ | | | | | | When none of the numbers get over 100, the width of the table was different. See https://github.com/coq/coq/pull/6736#issuecomment-365386802
* Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Maxime Dénès2018-01-08
|\
* | Trim more trailing whitespace in coq-makefile timing testGravatar Jason Gross2017-12-31
| | | | | | | | | | | | | | Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces
| * Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Jason Gross2017-12-27
| | | | | | | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
* | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
|/ | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* Do dependencies in 1 command per file class.Gravatar Gaëtan Gilbert2017-12-15
|
* Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Gravatar Maxime Dénès2017-11-28
|\
* \ Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵Gravatar Maxime Dénès2017-11-27
|\ \ | | | | | | | | | subdirectory.
| * | coq_makefile tests: build in easily removed temporary subdirectory.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | This allows us to avoid doing git clean.
| | * Fixing failing mkdir in test-suite for coq-makefile.Gravatar Hugo Herbelin2017-11-24
| |/ | | | | | | | | Calling the test a second time after a make clean was failing due to an existing "src" directory left by the first call.
* / Add test-suite tests for timing scriptsGravatar Jason Gross2017-11-22
|/ | | | | | | | | | | | | | | | | | | | | These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all *.log files, so we use *.log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per https://github.com/coq/coq/pull/6149#issuecomment-346410990)
* Have the coq_makefile timing test-suite print moreGravatar Jason Gross2017-11-17
| | | | | | This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
* Remove dependency of test-suite on git (fix #5725).Gravatar Théo Zimmermann2017-11-08
| | | | | | | The two lines that this commit remove are spurious as a `git clean -dfx || true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`.
* Handle ∞ in coq-makefile timing test-suiteGravatar Jason Gross2017-10-19
| | | | This should (hopefully) fix #5675.
* Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
| | | | | The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
* fix test-suite/coq-makefile/findlib-package on windowsGravatar Enrico Tassi2017-09-04
|
* coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsGravatar Enrico Tassi2017-08-29
|
* coq_makefile: use dedicated variable for extra packagesGravatar Enrico Tassi2017-08-29
| | | | | | | | | | CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
* coq_makefile: test using findlib's packageGravatar Enrico Tassi2017-08-29
|
* more verbose logs for coq-makefileGravatar Enrico Tassi2017-07-20
|
* coq-makefile: make test suite detect more errorsGravatar Enrico Tassi2017-07-20
| | | | Replacing ; with && and enabling bash's pipefail option
* Add timing scriptsGravatar Jason Gross2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.
* Remove dependency on -compat flag in coq_makefile test suite.Gravatar Maxime Dénès2017-06-15
|
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
* | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
* | Test-suite: do not test native compiler if disabled by configure.Gravatar Maxime Dénès2017-06-01
| |
| * test-suite/coq-makefile: we do not build byte file by default anymoreGravatar Pierre Letouzey2017-06-01
|/
* Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\
* \ Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Gravatar Maxime Dénès2017-05-28
|\ \
* \ \ Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \ \
| | | * Gitlab CIGravatar Gaëtan Gilbert2017-05-28
| | | |
| * | | coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| | |/ | |/| | | | | | | | | | | | | | | | | | | It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
* | | Add execution permission to test-suite file.Gravatar Théo Zimmermann2017-05-27
| | |
* | | Use specific shell for more robustness.Gravatar Théo Zimmermann2017-05-27
| | |
* | | Fix test-suite/coq-makefile on NixOS.Gravatar Théo Zimmermann2017-05-27
|/ /
| * Changes to make coq-makefile not failing on MacOS X.Gravatar Hugo Herbelin2017-05-26
|/ | | | There is still however a failure with "rmdir --ignore-fail-on-non-empty".
* add the only targetGravatar Enrico Tassi2017-05-23
| | | | | | | | This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
* coq_makefile: don't quote extra arguments (-arg)Gravatar Enrico Tassi2017-05-23
| | | | Restores compatibility with 8.6
* test suite for coq_makefile2Gravatar Enrico Tassi2017-05-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 11:02:54 +0000