coq/dev/bench, branch master The formal proof system Attempt to fix the bench after coq-core split 2021-03-07T11:37:07+00:00 Gaëtan Gilbert 2021-03-07T11:37:07+00:00 3404069faab82af02622823f0fac4d6800b0f5dd 






[bench] Re-enable coq-performance-tests
2021-02-03T15:13:00+00:00

Jason Gross

2021-02-03T15:13:00+00:00

51699a1dec7f1252fb9aaf7a1e7605bef95782da

Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04.
coq-performance-tests was fixed in
https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1.

Note that the current state is not optimal, as the bench does not test
the native compiler at all (see #13807).





Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04.
coq-performance-tests was fixed in
https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1.

Note that the current state is not optimal, as the bench does not test
the native compiler at all (see #13807).







Add VST to the set of default bench packages.
2021-02-02T19:37:50+00:00

Pierre-Marie Pédrot

2021-02-02T19:37:50+00:00

8758950929d5dc0474b68af52402c509851304e2












Merge PR #13805: Bench: remove broken packages
2021-02-02T19:01:08+00:00

Pierre-Marie Pédrot

2021-02-02T19:01:08+00:00

16244badc6e2bbbc4ab68c23066903a5390e4d56

Reviewed-by: ppedrot





Reviewed-by: ppedrot







Bench: don't uselessly rely on initialized opam
2021-02-02T14:11:22+00:00

Gaëtan Gilbert

2021-01-26T13:11:48+00:00

2284e8481e7eb3489ff25b5f5c896c7b95c383ee

AFAICT this init.sh call is useless.





AFAICT this init.sh call is useless.







Bench: remove broken packages
2021-01-29T13:13:21+00:00

Gaëtan Gilbert

2021-01-29T13:13:21+00:00

6f4c61d152ad801bd571088ab99eb276b0085a04

performance-tests and sf-plf have been failing for a long time without
updates, there's no point wasting time partally building them.





performance-tests and sf-plf have been failing for a long time without
updates, there's no point wasting time partally building them.







Bench: add .log extension to .stdout/stderr files
2020-12-11T11:17:44+00:00

Gaëtan Gilbert

2020-12-11T11:17:44+00:00

b98d4349907ccbb01d5fe5ea69d7923c6a6d3c63

Hopefully this allows viewing online with a download dialog on gitlab.





Hopefully this allows viewing online with a download dialog on gitlab.







Merge PR #13420: Modular printing algorithm for bench/render_results.
2020-11-24T14:12:35+00:00

coqbot-app[bot]

2020-11-24T14:12:35+00:00

fa70203a836b0b4482a9d053af1af438cc0b4240

Reviewed-by: SkySkimmer





Reviewed-by: SkySkimmer







add perennial to benchmark suite
2020-11-20T14:11:44+00:00

Ralf Jung

2020-10-21T13:15:51+00:00

6188353cfcf7f34ac591cff804764363c7987814












Modular printing algorithm for bench/render_results.
2020-11-19T15:22:34+00:00

Pierre-Marie Pédrot

2020-11-19T12:31:15+00:00

5bda98c882131dd35f81313d83a9e73e2a25a416

The old code was a mess of handwritten ad-hoc code to print the result table
in a fancy way. Instead of hardcoding everything this patch introduces a
generic function to print a table of data. This will allow extension of the
profiling information displayed to the user in an easy way.





The old code was a mess of handwritten ad-hoc code to print the result table
in a fancy way. Instead of hardcoding everything this patch introduces a
generic function to print a table of data. This will allow extension of the
profiling information displayed to the user in an easy way.