Karl Palmskog (Nov 30 2020 at 10:47): 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.
Enrico Tassi (Nov 30 2020 at 10:48):Why not, put also Pierre Marie in the loop
Enrico Tassi (Nov 30 2020 at 10:48):(sorry, for seme reasons I thought it was a private message)
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?
Pierre-Marie Pédrot (Nov 30 2020 at 10:49):Indeed.
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.
Pierre-Marie Pédrot (Nov 30 2020 at 10:50):I have a script called coqobjinfo somewhere that dumps metadata of vo files
Pierre-Marie Pédrot (Nov 30 2020 at 10:50):similar to ocamlobjinfo
Karl Palmskog (Nov 30 2020 at 10:50):basically, I need to extract where in the source file the .vio task comes from
Pierre-Marie Pédrot (Nov 30 2020 at 10:50):Yep, this is not really votour material if you need locations.
Karl Palmskog (Nov 30 2020 at 10:51):we had a branch summer 2019 which did that very barebones by modifying votour code
Pierre-Marie Pédrot (Nov 30 2020 at 10:51):But it should be easy to do.
Pierre-Marie Pédrot (Nov 30 2020 at 10:51):Is that information stored anywhere currently?
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)
Pierre-Marie Pédrot (Nov 30 2020 at 10:51):Or did you have to enrich the list of STM tasks?
Enrico Tassi (Nov 30 2020 at 10:51):yes
Karl Palmskog (Nov 30 2020 at 10:51):I can dig up the draft PR
Enrico Tassi (Nov 30 2020 at 10:52):it was on Coq, shouldn't be hard
Karl Palmskog (Nov 30 2020 at 10:52):I take responsibility for dropping the ball
Karl Palmskog (Nov 30 2020 at 10:52):https://github.com/coq/coq/pull/10333
Pierre-Marie Pédrot (Nov 30 2020 at 10:52):Looks reasonable.
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.
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
Pierre-Marie Pédrot (Nov 30 2020 at 10:53):Yes, I agree.
Karl Palmskog (Nov 30 2020 at 10:53):it doesn't matter if it's votour or something else bundled with Coq
Pierre-Marie Pédrot (Nov 30 2020 at 10:53):Right right.
Pierre-Marie Pédrot (Nov 30 2020 at 10:53):You know about ocamlobjinfo right?
Karl Palmskog (Nov 30 2020 at 10:54):I think I've heard about it, but never tried it
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.
Pierre-Marie Pédrot (Nov 30 2020 at 10:54):Adding vio metadata is easy.
Karl Palmskog (Nov 30 2020 at 10:55):but that is a separate program, right? Is it installed with Coq like votour?
Pierre-Marie Pédrot (Nov 30 2020 at 10:55):Just tell me when you want to discuss this.
Pierre-Marie Pédrot (Nov 30 2020 at 10:55):Yeah, it's a stupid ML file.
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
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
Karl Palmskog (Nov 30 2020 at 10:57):maybe one could turn the ML file into a full fledged CLI utility then?
Pierre-Marie Pédrot (Nov 30 2020 at 10:59):Indeed, indeed.
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
Enrico Tassi (Nov 30 2020 at 11:17):ok
Pierre-Marie Pédrot (Nov 30 2020 at 11:20):fine with me
Karl Palmskog (Dec 01 2020 at 11:08):ping @Enrico Tassi
Karl Palmskog (Dec 01 2020 at 11:10):Emilio suggests using PPX output instead of lots of printfs
Pierre-Marie Pédrot (Dec 01 2020 at 11:11):For what exactly? Also, PPX are there own can of worms.
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
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?
Pierre-Marie Pédrot (Dec 01 2020 at 11:18):The major interest of metadata dumping is precisely to get cross-language interfaces
Karl Palmskog (Dec 01 2020 at 11:18):the problem is that the output has to be persisted on disk
Pierre-Marie Pédrot (Dec 01 2020 at 11:19):But this is orthogonal to the information extraction, isn't it?
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
Karl Palmskog (Dec 01 2020 at 11:20):PPX is to me a sort of cross-language interface
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?
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.
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...
Pierre-Marie Pédrot (Dec 01 2020 at 11:23):Right.
Karl Palmskog (Dec 01 2020 at 11:24):I'm not adamant about PPX, just something that was discussed
Enrico Tassi (Dec 01 2020 at 11:29):PPX is just a cheap way to print json or sexp
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.
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.
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.
Michael Soegtrop (Dec 02 2020 at 13:10):Out of curiosity: what is votour?
Pierre-Marie Pédrot (Dec 02 2020 at 13:12):A program to inspect the binary data contained in a v(i)o
Michael Soegtrop (Dec 02 2020 at 13:13):Does it dump the contents of a .vo file into say XML?
Pierre-Marie Pédrot (Dec 02 2020 at 13:13):No, but you could. Although that would be very big.
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
Michael Soegtrop (Dec 02 2020 at 13:14):OK - I put it on my reading list
Enrico Tassi (Dec 02 2020 at 13:20):trivia: "votour" sounds like "vulture", it's a bird joke by Pierre L.
Karl Palmskog (Dec 03 2020 at 09:33):@Enrico Tassi @Pierre-Marie Pédrot am in room 4 now in BBB
Enrico Tassi (Dec 03 2020 at 09:34):sorry, 5 minutes
Enrico Tassi (Dec 03 2020 at 09:34):we are in 1
Pierre-Marie Pédrot (Dec 03 2020 at 09:38):@Enrico Tassi should we leave room 1?
Enrico Tassi (Dec 03 2020 at 09:39):yup
Enrico Tassi (Dec 03 2020 at 09:39):I'm leaving
Pierre-Marie Pédrot (Dec 03 2020 at 10:23):dune is already getting in the way -_-
Gaëtan Gilbert (Dec 03 2020 at 10:24):specifics?
Pierre-Marie Pédrot (Dec 03 2020 at 10:24):copy-pasting the coqc stanza was not enough
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
Pierre-Marie Pédrot (Dec 03 2020 at 10:25):replacing the names accordingly
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.
There is a module field, so I don't know what I can do more.
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))
Any idea?
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 \)
Gaëtan Gilbert (Dec 03 2020 at 10:31):not sure why it's written that way
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
Gaëtan Gilbert (Dec 03 2020 at 10:37):dune build _build/default/topbin/mything.exe
Pierre-Marie Pédrot (Dec 03 2020 at 10:37):nothing shorter?
Gaëtan Gilbert (Dec 03 2020 at 10:37):dune build _build/install/default/bin/mything
Gaëtan Gilbert (Dec 03 2020 at 10:38):dune exec mything.exe might work
Pierre-Marie Pédrot (Dec 03 2020 at 10:38):what's the point of giving that crapload of metadata name then?
Pierre-Marie Pédrot (Dec 03 2020 at 10:40):Very nice 6Mio binary generated out of an empty file by the way.
Gaëtan Gilbert (Dec 03 2020 at 10:41):you asked for it with -linkall, don't complain
Pierre-Marie Pédrot (Dec 03 2020 at 10:42):I've asked to only link coq.lib
Pierre-Marie Pédrot (Dec 03 2020 at 10:42):Don't tell me coq.lib is already 6Mio?!
Gaëtan Gilbert (Dec 03 2020 at 10:44):if I remove linkall I get 2.2MB
Pierre-Marie Pédrot (Dec 03 2020 at 10:45):Still humongous.
Gaëtan Gilbert (Dec 03 2020 at 10:45):if I remove both coq.lib and lnkall I get 1.1MB
Pierre-Marie Pédrot (Dec 03 2020 at 10:45):Dafuq?
Pierre-Marie Pédrot (Dec 03 2020 at 10:45):The OCaml runtime has become bloated, seriously.
Gaëtan Gilbert (Dec 03 2020 at 10:49):(1.1MB is the same that I get from direct ocamlopt on empty file)
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
Pierre-Marie Pédrot (Dec 03 2020 at 10:49):there are bigarrays in an empty OCaml program?!
Gaëtan Gilbert (Dec 03 2020 at 10:50):@not enough memory
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
Pierre-Marie Pédrot (Dec 03 2020 at 11:06):Ah, that means OCaml is now Desktop-ready. Let's rejoice!
Emilio Jesús Gallego Arias (Dec 03 2020 at 13:08):You can try removing -g from the default flags
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
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: Jun 11 2023 at 01:30 UTC