@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.
Why not, put also Pierre Marie in the loop
(sorry, for seme reasons I thought it was a private message)
@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?
I am not sure votour is the right tool for that, though. It's a bit too low-level.
I have a script called coqobjinfo somewhere that dumps metadata of vo files
similar to ocamlobjinfo
basically, I need to extract where in the source file the
.vio task comes from
Yep, this is not really votour material if you need locations.
we had a branch summer 2019 which did that very barebones by modifying
But it should be easy to do.
Is that information stored anywhere currently?
there is probably still a PR (since the piece of info has to be stored in the .vo in the first place)
Or did you have to enrich the list of STM tasks?
I can dig up the draft PR
it was on Coq, shouldn't be hard
I take responsibility for dropping the ball
I can dig up my coqobjinfo script, should be easy to add this kind of metadata.
the idea is that there needs to be some CLI tool where I can get that info
Yes, I agree.
it doesn't matter if it's
votour or something else bundled with Coq
You know about ocamlobjinfo right?
I think I've heard about it, but never tried it
The Coq variant was outputting similar stuff, like the list of dependencies and their hash, the list of proofs stored, and so on.
Adding vio metadata is easy.
but that is a separate program, right? Is it installed with Coq like
Just tell me when you want to discuss this.
Yeah, it's a stupid ML file.
I think the ideal would be after my planned plenary, where I give the high-level idea, so for example, any time Thursday
It's not part of Coq currently but I did use it from time to time for dirty scripts not using OCaml
maybe one could turn the ML file into a full fledged CLI utility then?
@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
fine with me
ping @Enrico Tassi
Emilio suggests using PPX output instead of lots of printfs
For what exactly? Also, PPX are there own can of worms.
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
In that case I don't really see the interest of serializing, why don't you link directly to the underlying library?
The major interest of metadata dumping is precisely to get cross-language interfaces
the problem is that the output has to be persisted on disk
But this is orthogonal to the information extraction, isn't it?
basically, our workflow is that we invoke a Coq regression proving run, then persist metadata to stable storage
PPX is to me a sort of cross-language interface
You would be happy if we simply exported an OCaml API to access v(i)o metadata, right?
You can have your PPX schonabulator on your side, you just link to the OCaml API to read the data.
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...
I'm not adamant about PPX, just something that was discussed
PPX is just a cheap way to print json or sexp
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.
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.
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.
Out of curiosity: what is votour?
A program to inspect the binary data contained in a v(i)o
Does it dump the contents of a .vo file into say XML?
No, but you could. Although that would be very big.
It's interactive, it lets you crawl the OCaml data from the vo with various metadata info and nice printers when available
OK - I put it on my reading list
trivia: "votour" sounds like "vulture", it's a bird joke by Pierre L.
@Enrico Tassi @Pierre-Marie Pédrot am in room 4 now in BBB
sorry, 5 minutes
we are in 1
@Enrico Tassi should we leave room 1?
dune is already getting in the way -_-
copy-pasting the coqc stanza was not enough
@Gaëtan Gilbert I am trying to introduce a new binary, so I copy-pasted the one for coqtop
replacing the names accordingly
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.
the code is
(executable (name coqobjinfo_bin) (public_name coqobjinfo) (package coq) (modules coqobjinfo_bin) (libraries coq.lib) (link_flags -linkall))
(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 \)
not sure why it's written that way
dear dune hotline, how do I generate that binary after? My knowledge of dune stops at
make -f Makefile.dune states
dune build _build/default/topbin/mything.exe
dune build _build/install/default/bin/mything
dune exec mything.exe might work
what's the point of giving that crapload of metadata name then?
Very nice 6Mio binary generated out of an empty file by the way.
you asked for it with -linkall, don't complain
I've asked to only link coq.lib
Don't tell me coq.lib is already 6Mio?!
if I remove linkall I get 2.2MB
if I remove both coq.lib and lnkall I get 1.1MB
The OCaml runtime has become bloated, seriously.
(1.1MB is the same that I get from direct ocamlopt on empty file)
slightly off-topic, but
touch foo.ml && ocamlopt -o foo foo.ml && strings foo | less is terrifying
there are bigarrays in an empty OCaml program?!
@not enough memory
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
Ah, that means OCaml is now Desktop-ready. Let's rejoice!
You can try removing
-g from the default flags
linkall is a pain indeed, I tried to remove it but my proposal didn't go thu :S
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