Stream: Coq devs & plugin devs

Topic: combined coq binaries


view this post on Zulip Gaëtan Gilbert (May 07 2024 at 15:29):

there was at some point discussion about combining some of the coq binaries to save on installation size
I guess the idea was that instead of having coqc/coqtop/coqfooworker each statically linking coq-core.toplevel + dependencies at currently ~29MB each, we would have some coqmain binary linking them and some lightweight shims for coqc etc using it to provide the functionality

I tried playing with it a bit and I'm not sure how best to make it work. Possible methods and problems:

thoughts?

view this post on Zulip Guillaume Melquiond (May 07 2024 at 15:44):

For Why3, we use the .cmxs approach, but the other way around. That is, why3 is a large binary that statically links why3.cmxa, while all the tools are small .cmxs files that are loaded on the fly and link into it. For example, why3 prove is comprised from why3 (18MB) and why3prove.cmxs (15kB).

view this post on Zulip Gaëtan Gilbert (May 07 2024 at 16:07):

forgot an option:

view this post on Zulip Jason Gross (May 08 2024 at 00:15):

What about this?
Instead of dispatching based on argv.(0), have coqmain be coq that can do coq coqc foo.v, coq coqtop, etc.
Then distribute a shell script on Linux/Unix/Mac for coqc, coqtop, etc that assumes coq is in the same directory as the script and does exec "$(dirname "$0")/coq" coqc "$@" or whatever. Windows can get either a .ps1, .bat, or the minimal OCaml program (or it could be a minimal C program, whatever).

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2024 at 11:40):

That seems too complex to me for the space gains.

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2024 at 11:41):

In particular as we consider the workers to be "deprecated"

view this post on Zulip Emilio Jesús Gallego Arias (May 08 2024 at 11:42):

So in a sense we need to ship coqc and coqtop, that's two binaries, and they are actually IMHO quite different (IMO the needs of an interactive shell are quite different in terms for example of also wanting to have nice terminal libs, etc...)

So if coqtop is annoying, we could place it in a coq-coqtop opam package

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2024 at 12:30):

These seem to me like reasonable binary size:

-r-xr-xr-x 2 egallego picube 27M mai    2 19:14 _build/default/vendor/coq/topbin/coqc_bin.exe
-r-xr-xr-x 2 egallego picube 11M mai    2 19:14 _build/default/vendor/coq/topbin/coqnative_bin.exe
-r-xr-xr-x 2 egallego picube 27M mai    2 19:14 _build/default/vendor/coq/topbin/coqtop_bin.exe
-r-xr-xr-x 2 egallego picube 27M mai    2 19:14 _build/default/vendor/coq/topbin/coqworker_bin.exe

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2024 at 12:32):

Gaëtan Gilbert said:

forgot an option:

In the end this seems like the way most other tools go, having a single command, and then it is often simple to just dispatch. Only in special cases you may want to spawn some process or do some esoteric linking IMO.

view this post on Zulip Gaëtan Gilbert (May 09 2024 at 12:41):

I guess when we change the binary names to rocq it could be a good opportunity to do this too

view this post on Zulip Théo Zimmermann (May 14 2024 at 12:55):

Yes, and the compatibility scripts / binaries could be small wrappers that call rocq.


Last updated: Oct 13 2024 at 01:02 UTC