Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
510e1d40
Commit
510e1d40
authored
Jan 28, 2020
by
POTTIER Francois
Browse files
New entry [make timings] to produce timing data. New R script to process it (untested).
parent
384e8dec
Pipeline
#116815
passed with stages
in 26 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
510e1d40
*~
.merlin
_build
timings.csv
Makefile
View file @
510e1d40
...
...
@@ -38,6 +38,29 @@ export CDPATH=
test
:
@
dune build
--display
short @test
# [make timings] extracts the performance data gathered by [make test].
# Be careful: this data is not high quality, and is machine-dependent.
# We select just one line in the performance data printed by [menhir
# --timings-to <filename>]. The variable $field indicates which field
# we are interested in.
.PHONY
:
timings
timings
:
test
@
\
field
=
"Construction of the LR(1) automaton"
;
\
(
\
echo
"name,states,time"
&&
\
cd
_build/default/test/static/src
&&
\
for
f
in
*
.out.timings
;
do
\
name
=
$
${f%.out.timings}
;
\
states
=
`
sed
-n
-e
"s/^Built an LR(1) automaton with
\(
[0-9]
\+\)
states./
\1
/p"
$
${f%.timings}
`
;
\
time
=
`
sed
-n
-e
"s/^
$$
field:
\(
.*
\)
/
\1
/p"
$$
f
`
;
\
echo
"
$$
name,
$$
states,
$$
time"
;
\
done
\
)
>
timings.csv
@
./timings.r
# [make speed] runs the speed test in test/dynamic/speed.
.PHONY
:
speed
...
...
timings.r
0 → 100755
View file @
510e1d40
#!/usr/bin/env Rscript
require
(
ggplot2
)
# Our working directory.
pwd
<-
"."
# Load our data.
mydata
<-
read.csv
(
paste
(
pwd
,
"timings.csv"
,
sep
=
"/"
))
# Restrict ourselves to a subset of the data.
mydata
<-
subset
(
mydata
,
time
>=
0.25
)
# A function which saves a plot to a PDF file.
save
<-
function
(
filename
)
{
ggsave
(
paste
(
pwd
,
filename
,
sep
=
"/"
),
width
=
12
,
height
=
8
,
units
=
"cm"
)
}
# A function that creates a scatter plot. Data on the X and Y axes
# is determined by the argument [xy]. The scale is logarithmic.
# [lx] and [ly] are labels for the axes.
plotloglog
<-
function
(
xy
,
lx
,
ly
)
{
ggplot
(
mydata
,
xy
)
+
geom_point
(
size
=
3
)
+
scale_x_log10
()
+
scale_y_log10
()
+
xlab
(
lx
)
+
ylab
(
ly
)
}
# Scatter plots.
plotloglog
(
aes
(
x
=
states
,
y
=
time
),
"# states"
,
"time (seconds)"
)
save
(
"states-time.pdf"
)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment