Stream: Coq devs & plugin devs

Topic: How to reuse OCaml script stuff


view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:25):

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?

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:26):

I went for an overly aggressive solution atm of putting the table module in clib, but this is probably not what we want.

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:27):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:27):

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

view this post on Zulip Ali Caglayan (Mar 04 2022 at 18:50):

When I do this it doesn't work: https://gitlab.com/coq/coq/-/jobs/2165327505

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:11):

Isn't dune exec meant to be emulating installing then running a binary? How does this make sense for a dev script?

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:12):

ping @Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:16):

I think it does not

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:16):

binaries are special ttbomk

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:16):

I'm not sure what the question is tho

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:22):

How can I run an ml script if I won't install it?

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:23):

Configure for example gets installed so it is unambiguous when you write dune exec -- configure.exe right?

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:23):

But I have not been able to get my own executable running this way

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:23):

Only if I know the exact path

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:25):

So dune exec -- tools/configure.exe would be the correct thing, but how would you run this from say dev?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:26):

Yes, you can use the path, or use the (bin ) stanza to put the binary in scope

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:27):

in (env )

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:27):

Ali Caglayan said:

So dune exec -- tools/configure.exe would be the correct thing, but how would you run this from say dev?

what do you mean?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:27):

in fact configure is run using the concrete path, it is not installed

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:28):

check configure

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:54):

Sorry @Ali Caglayan I missed the context about, can you point me to the exact code doing the call that fails?

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:55):

https://github.com/coq/coq/blob/1707ddcef638dcdecaad5e298047762519b4b098/dev/bench/bench.sh#L20-L25

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:56):

https://gitlab.com/coq/coq/-/jobs/2165327505

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:56):

Thats what happened

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:56):

It says program not found

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:56):

So I am guessing I did the path wrong

view this post on Zulip Ali Caglayan (Mar 08 2022 at 21:56):

What is the correct way to call this?

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 21:57):

not sure the bench executes in a context where dune is available

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:59):

could be something as silly as being in the wrong directory

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:59):

maybe do a pwd before?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:59):

also do ls /home/gitlab-runner/builds/av_eR6za/0/coq/coq

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:59):

keep in mind that dune is a bit messy in terms of how it detects the root

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:00):

we did mess things up and now we do pass --root . always

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:00):

there are improvements planned on this, but dune can change roots sometimes when you don't want, specially dune 2.x

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:00):

@Gaëtan Gilbert Looks like dune is available and working, i just can't use it right it seems

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:01):

@Ali Caglayan for sure it is a path problem

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:01):

Is there a way to do this path agnostically?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:01):

please add a few pwd and ls for debug

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:01):

Ali Caglayan said:

Is there a way to do this path agnostically?

if we are facing the root detection problem not

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 22:01):

does it work when you run the dune exec locally?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:01):

well, yes, but we need to be aware

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 22:01):

on your machine?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:02):

the problem with root detection is that it is triggered if a dune-project is found in upper directories

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:02):

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

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:03):

Works on my machine, but only when I call from the project root

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:03):

I have no idea where the bench is calling it

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:03):

Let me see

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:03):

for that you can use

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:03):

(env (bin))

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:03):

Also I had to actually go into dev/bench and build everything there

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:03):

doesn't look like dune build picked it up

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:03):

there is a more interesting way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:03):

which is to call the binary from a rule

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:04):

so instead of dune exec you use dune build foo/bench-log

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:04):

or an alias dune build @bench-log

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:04):

Ali Caglayan said:

doesn't look like dune build picked it up

that's bizarre

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:05):

it is "pure" in that sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:05):

so that's why rules are usually better if you wanna declare other deps

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:06):

this stuff is not so intutitive because of the implicit source rule xd

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:06):

but I can see that having to add rules for .ml sources would be a PITA

view this post on Zulip Ali Caglayan (Mar 08 2022 at 22:07):

Let's see what happens: https://gitlab.com/coq/coq/-/jobs/2179161225

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 22:09):

we may cd _bench or something at some point

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 22:09):

I guess you should add --root $program_path/../..

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 22:21):

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

view this post on Zulip Ali Caglayan (Mar 09 2022 at 13:46):

Aha setting the root fixed my problems

view this post on Zulip Ali Caglayan (Mar 09 2022 at 13:46):

It's working now :)) https://gitlab.com/coq/coq/-/jobs/2182001701

view this post on Zulip Gaëtan Gilbert (Mar 09 2022 at 13:55):

the precision is kinda annoying
jq -n '0.2 - 0.3' says -0.09999999999999998
echo '0.2 - 0.3' | bc says -.1

view this post on Zulip Ali Caglayan (Mar 09 2022 at 13:58):

Yep I saw that too

view this post on Zulip Ali Caglayan (Mar 09 2022 at 13:58):

I don't know what jq is doing here

view this post on Zulip Ali Caglayan (Mar 09 2022 at 13:59):

I considered truncating it, but maybe we should just handle it all in OCaml

view this post on Zulip Ali Caglayan (Mar 09 2022 at 14:03):

@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?

view this post on Zulip Gaëtan Gilbert (Mar 09 2022 at 14:27):

stdlib probably doesn't generate the line timings

view this post on Zulip Ali Caglayan (Mar 10 2022 at 03:11):

It works! :-) https://gitlab.com/coq/coq/-/jobs/2185241374

view this post on Zulip Ali Caglayan (Mar 10 2022 at 13:28):

At least the table is formatted correctly, the contents are garbage atm but I am fixing it


Last updated: Feb 06 2023 at 00:03 UTC