coq/test-suite/coq-makefile/timing/precomputed-time-tests/.gitattributes, branch master The formal proof system Add test-suite tests for timing scripts 2017-11-22T21:20:00+00:00 Jason Gross 2017-11-22T17:27:34+00:00 e87c3f9da4dbc3b876e2662c122c17141b7feae5 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) 
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)