Stream: CUDW 2020

Topic: votour improvements


view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:47):

@Enrico Tassi can we book some time to discuss adding features to votour? Recall the last workshop. I was hoping to revive that work for 8.14.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:48):

Why not, put also Pierre Marie in the loop

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:48):

(sorry, for seme reasons I thought it was a private message)

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:49):

@Pierre-Marie Pédrot Enrico and I are planning to do some work on improving votour, specifically to allow querying .vio files (and maybe also vos?) Is this something you could advise on as well?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:49):

Indeed.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:50):

I am not sure votour is the right tool for that, though. It's a bit too low-level.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:50):

I have a script called coqobjinfo somewhere that dumps metadata of vo files

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:50):

similar to ocamlobjinfo

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:50):

basically, I need to extract where in the source file the .vio task comes from

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:50):

Yep, this is not really votour material if you need locations.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:51):

we had a branch summer 2019 which did that very barebones by modifying votour code

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:51):

But it should be easy to do.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:51):

Is that information stored anywhere currently?

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:51):

there is probably still a PR (since the piece of info has to be stored in the .vo in the first place)

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:51):

Or did you have to enrich the list of STM tasks?

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:51):

yes

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:51):

I can dig up the draft PR

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:52):

it was on Coq, shouldn't be hard

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:52):

I take responsibility for dropping the ball

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:52):

https://github.com/coq/coq/pull/10333

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:52):

Looks reasonable.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:53):

I can dig up my coqobjinfo script, should be easy to add this kind of metadata.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:53):

the idea is that there needs to be some CLI tool where I can get that info

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:53):

Yes, I agree.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:53):

it doesn't matter if it's votour or something else bundled with Coq

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:53):

Right right.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:53):

You know about ocamlobjinfo right?

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:54):

I think I've heard about it, but never tried it

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:54):

The Coq variant was outputting similar stuff, like the list of dependencies and their hash, the list of proofs stored, and so on.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:54):

Adding vio metadata is easy.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:55):

but that is a separate program, right? Is it installed with Coq like votour?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:55):

Just tell me when you want to discuss this.

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:55):

Yeah, it's a stupid ML file.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:55):

I think the ideal would be after my planned plenary, where I give the high-level idea, so for example, any time Thursday

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:55):

It's not part of Coq currently but I did use it from time to time for dirty scripts not using OCaml

view this post on Zulip Karl Palmskog (Nov 30 2020 at 10:57):

maybe one could turn the ML file into a full fledged CLI utility then?

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 10:59):

Indeed, indeed.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 11:04):

@Pierre-Marie Pédrot @Enrico Tassi how about a breakout room session on 10:30am on Thursday? Then I will have time to figure out where we were with the PR and look at the ML file

view this post on Zulip Enrico Tassi (Nov 30 2020 at 11:17):

ok

view this post on Zulip Pierre-Marie Pédrot (Nov 30 2020 at 11:20):

fine with me

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:08):

ping @Enrico Tassi

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:10):

Emilio suggests using PPX output instead of lots of printfs

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:11):

For what exactly? Also, PPX are there own can of worms.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:16):

the idea is that the output of coqobjdump (or whatever it will be called) has to be parsed by other OCaml tools. So instead of coming up with some clever output format, one could just serialize some simple datastructures, and have the other tools deserialize them

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:17):

In that case I don't really see the interest of serializing, why don't you link directly to the underlying library?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:18):

The major interest of metadata dumping is precisely to get cross-language interfaces

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:18):

the problem is that the output has to be persisted on disk

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:19):

But this is orthogonal to the information extraction, isn't it?

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:19):

basically, our workflow is that we invoke a Coq regression proving run, then persist metadata to stable storage

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:20):

PPX is to me a sort of cross-language interface

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:20):

You would be happy if we simply exported an OCaml API to access v(i)o metadata, right?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:21):

You can have your PPX schonabulator on your side, you just link to the OCaml API to read the data.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:22):

the drawback is that I would have to bundle my own OCaml utility everywhere, so if we could find some compromise where the v(i)o metadata is output by a tool bundled with Coq, that would be better...

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:23):

Right.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 11:24):

I'm not adamant about PPX, just something that was discussed

view this post on Zulip Enrico Tassi (Dec 01 2020 at 11:29):

PPX is just a cheap way to print json or sexp

view this post on Zulip Enrico Tassi (Dec 01 2020 at 11:30):

It's a huge, ugly, stack of software. I use them extensively in Elpi, so I know the drill. IMO for an external tool they are acceptable. But I really don't know which data you need exactly. If you nee "FILE:LINE" then I don't see the point of PPX either.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 11:32):

Last, PPX a la serapi makes you code depend on the data representation we have in Coq, if we change it (e.g. swap two fields of a tule), your code breaks. So I'd use PPX on an intermediate, docuemented, data structure, not on the ones we have in Coq.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 11:34):

Imo the "API" would be an ocaml data type, a brand new one, plus a serialization format (say sexp). Then we write OCaml code to make out internal crap to that API, and we keep it working in CI. Printing that API to sexp can be done via PPX imo.

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 13:10):

Out of curiosity: what is votour?

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 13:12):

A program to inspect the binary data contained in a v(i)o

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 13:13):

Does it dump the contents of a .vo file into say XML?

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 13:13):

No, but you could. Although that would be very big.

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2020 at 13:13):

It's interactive, it lets you crawl the OCaml data from the vo with various metadata info and nice printers when available

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 13:14):

OK - I put it on my reading list

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:20):

trivia: "votour" sounds like "vulture", it's a bird joke by Pierre L.

view this post on Zulip Karl Palmskog (Dec 03 2020 at 09:33):

@Enrico Tassi @Pierre-Marie Pédrot am in room 4 now in BBB

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:34):

sorry, 5 minutes

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:34):

we are in 1

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 09:38):

@Enrico Tassi should we leave room 1?

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:39):

yup

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:39):

I'm leaving

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:23):

dune is already getting in the way -_-

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:24):

specifics?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:24):

copy-pasting the coqc stanza was not enough

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:24):

@Gaëtan Gilbert I am trying to introduce a new binary, so I copy-pasted the one for coqtop

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:25):

replacing the names accordingly

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:25):

And I get

File "topbin/dune", line 1, characters 0-0:
Error: Module "Coqobjinfo_bin" is used in several stanzas:
- topbin/dune:39
- topbin/dune:48
To fix this error, you must specify an explicit "modules" field in every
library, executable, and executables stanzas in this dune file. Note that
each module cannot appear in more than one "modules" field - it must belong
to a single library or executable.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:25):

There is a module field, so I don't know what I can do more.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:26):

the code is

(executable
 (name coqobjinfo_bin)
 (public_name coqobjinfo)
 (package coq)
 (modules coqobjinfo_bin)
 (libraries coq.lib)
 (link_flags -linkall))

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:28):

Any idea?

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:30):

in

(executables
 (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin)
 (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt)
 (package coq)
 (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin)
 (libraries coq.toplevel)
 (link_flags -linkall))

you need to add the module to the exclusions (after the \)

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:31):

not sure why it's written that way

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:35):

dear dune hotline, how do I generate that binary after? My knowledge of dune stops at make -f Makefile.dune states

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:37):

dune build _build/default/topbin/mything.exe

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:37):

nothing shorter?

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:37):

dune build _build/install/default/bin/mything

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:38):

dune exec mything.exe might work

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:38):

what's the point of giving that crapload of metadata name then?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:40):

Very nice 6Mio binary generated out of an empty file by the way.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:41):

you asked for it with -linkall, don't complain

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:42):

I've asked to only link coq.lib

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:42):

Don't tell me coq.lib is already 6Mio?!

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:44):

if I remove linkall I get 2.2MB

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:45):

Still humongous.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:45):

if I remove both coq.lib and lnkall I get 1.1MB

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:45):

Dafuq?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:45):

The OCaml runtime has become bloated, seriously.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:49):

(1.1MB is the same that I get from direct ocamlopt on empty file)

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:49):

slightly off-topic, but touch foo.ml && ocamlopt -o foo foo.ml && strings foo | less is terrifying

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 10:49):

there are bigarrays in an empty OCaml program?!

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 10:50):

@not enough memory

view this post on Zulip Guillaume Melquiond (Dec 03 2020 at 11:02):

Yes. This is kind of frightening. The executable files for Why3 were taking about 250MB and users were complaining. So, I changed the whole build process so that the binaries are compiled as dumb .cmxs files (plus an actual executable that just load them). This brought the total size down to 24MB, so a 10x reduction. https://gitlab.inria.fr/why3/why3/-/issues/485

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 11:06):

Ah, that means OCaml is now Desktop-ready. Let's rejoice!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2020 at 13:08):

You can try removing -g from the default flags

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2020 at 13:09):

linkall is a pain indeed, I tried to remove it but my proposal didn't go thu :S

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2020 at 13:10):

As of today, we'd just need to put the tactics not used by coqc in the ltac plugin. Other option is to rework the dynamic linker but that requires ocamlfind linking support so it will take a while.


Last updated: Oct 16 2021 at 09:07 UTC