I am trying to print a table in my bench summary PR. Currently there is a nice OCaml formatter in the bench_results ocmal script written PMP. I would like to move this to a common library so I can call it from another script. However this goes against the pattern of out-of-the-box OCaml scripts. Should I move to a dune wrapper like configure?
I went for an overly aggressive solution atm of putting the table module in clib, but this is probably not what we want.
When I mean "move to a dune wrapper" I mean stop using the ocaml top level in a script and instead have a bash wrapper around dune exec.
Ali Caglayan said:
I went for an overly aggressive solution atm of putting the table module in clib, but this is probably not what we want.
I'd say just make that script an executable and add the dune file, it makes sense to me that this script could use some fancy json stuff eventually in opam
When I do this it doesn't work: https://gitlab.com/coq/coq/-/jobs/2165327505
Isn't dune exec meant to be emulating installing then running a binary? How does this make sense for a dev script?
ping @Emilio Jesús Gallego Arias
I think it does not
binaries are special ttbomk
I'm not sure what the question is tho
How can I run an ml script if I won't install it?
Configure for example gets installed so it is unambiguous when you write dune exec -- configure.exe
right?
But I have not been able to get my own executable running this way
Only if I know the exact path
So dune exec -- tools/configure.exe
would be the correct thing, but how would you run this from say dev
?
Yes, you can use the path, or use the (bin )
stanza to put the binary in scope
in (env )
Ali Caglayan said:
So
dune exec -- tools/configure.exe
would be the correct thing, but how would you run this from saydev
?
what do you mean?
in fact configure is run using the concrete path, it is not installed
check configure
Sorry @Ali Caglayan I missed the context about, can you point me to the exact code doing the call that fails?
https://github.com/coq/coq/blob/1707ddcef638dcdecaad5e298047762519b4b098/dev/bench/bench.sh#L20-L25
https://gitlab.com/coq/coq/-/jobs/2165327505
Thats what happened
It says program not found
So I am guessing I did the path wrong
What is the correct way to call this?
not sure the bench executes in a context where dune is available
could be something as silly as being in the wrong directory
maybe do a pwd before?
also do ls /home/gitlab-runner/builds/av_eR6za/0/coq/coq
keep in mind that dune is a bit messy in terms of how it detects the root
we did mess things up and now we do pass --root .
always
there are improvements planned on this, but dune can change roots sometimes when you don't want, specially dune 2.x
@Gaëtan Gilbert Looks like dune is available and working, i just can't use it right it seems
@Ali Caglayan for sure it is a path problem
Is there a way to do this path agnostically?
please add a few pwd and ls for debug
Ali Caglayan said:
Is there a way to do this path agnostically?
if we are facing the root detection problem not
does it work when you run the dune exec locally?
well, yes, but we need to be aware
on your machine?
the problem with root detection is that it is triggered if a dune-project
is found in upper directories
Ali Caglayan said:
Is there a way to do this path agnostically?
so the answer to this is: yes, but only after we can control the workspace dune is gonna be called from;
so you pay a "bootstrap" control cost
Works on my machine, but only when I call from the project root
I have no idea where the bench is calling it
Let me see
for that you can use
(env (bin))
Also I had to actually go into dev/bench and build everything there
doesn't look like dune build picked it up
there is a more interesting way
which is to call the binary from a rule
so instead of dune exec
you use dune build foo/bench-log
or an alias dune build @bench-log
Ali Caglayan said:
doesn't look like dune build picked it up
that's bizarre
well, remember that dune executes stuff in a sandbox, so of course if you don't build other files, they are not gonna be present
it is "pure" in that sense
so that's why rules are usually better if you wanna declare other deps
this stuff is not so intutitive because of the implicit source rule xd
but I can see that having to add rules for .ml sources would be a PITA
Let's see what happens: https://gitlab.com/coq/coq/-/jobs/2179161225
we may cd _bench or something at some point
I guess you should add --root $program_path/../..
Ali Caglayan said:
Let's see what happens: https://gitlab.com/coq/coq/-/jobs/2179161225
you need to fix the deps tho if they are still wrong, or else it'll keep failing
Aha setting the root fixed my problems
It's working now :)) https://gitlab.com/coq/coq/-/jobs/2182001701
the precision is kinda annoying
jq -n '0.2 - 0.3'
says -0.09999999999999998
echo '0.2 - 0.3' | bc
says -.1
Yep I saw that too
I don't know what jq is doing here
I considered truncating it, but maybe we should just handle it all in OCaml
@Gaëtan Gilbert Also we display bench results for the stdlib but don't include that in the html data, where can I find that info?
stdlib probably doesn't generate the line timings
It works! :-) https://gitlab.com/coq/coq/-/jobs/2185241374
At least the table is formatted correctly, the contents are garbage atm but I am fixing it
Last updated: Oct 13 2024 at 01:02 UTC