Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

building timing reports with dune #2234

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions dune
Original file line number Diff line number Diff line change
Expand Up @@ -129,3 +129,35 @@
(file file_to_bench))
(action
(run echo "Starting bench. This may take a while.")))

; Timing report

(rule
(alias timing-html-hint)
(deps (universe) %{bin:lua})
(action
(run echo "Generating timing report. This may take a while.")))

(rule
(alias timing-html)
(target
(dir timing-html))
(deps
(alias timing-html-hint)
etc/generate_coqproject.sh
etc/time2html
Makefile
Makefile.coq.local
Makefile.coq.local-early
(sandbox always)
(sandbox preserve_file_kind)
(glob_files_rec ./theories/*.v)
(glob_files_rec ./contrib/*.v)
(glob_files_rec ./test/*.v))
(action
(setenv
GENERATE_COQPROJECT_FOR_DUNE
true
(progn
(ignore-outputs
(run %{bin:make} timing-html))))))
2 changes: 2 additions & 0 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@

(generate_opam_files true)

(using directory-targets 0.1)

(source
(github HoTT/HoTT))

Expand Down
6 changes: 3 additions & 3 deletions etc/generate_coqproject.sh
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@ COQPROJECT_HEADER=\
if [ "$GENERATE_COQPROJECT_FOR_DUNE" == "true" ]; then
COQPROJECT_HEADER="$COQPROJECT_HEADER
# Dune compatibility
-R _build/default/theories HoTT
-Q _build/default/contrib HoTT.Contrib
-Q _build/default/test HoTT.Tests
-R $PWD/theories HoTT
-Q $PWD/contrib HoTT.Contrib
-Q $PWD/test HoTT.Tests
"
fi

Expand Down
Loading