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:
exec
s coqmain with an extra --mode=coqc
argument -> locating coqmain could be a bit tricky, minimal ocaml programs seem not that small (empty foo.ml produces 1MB executable, we may get 2 / 3MB for the shim)exec
s coqmain with --mode=coqc
-> same issues with locating coqmain as previous point, not very windows compatiblethoughts?
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).
forgot an option:
coq
which can be invoked as coq coqc foo.v
coq coqtop
etc -> easy to implement but breaks backwards compatWhat 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).
That seems too complex to me for the space gains.
In particular as we consider the workers to be "deprecated"
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
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
Gaëtan Gilbert said:
forgot an option:
- there is no coqc, only
coq
which can be invoked ascoq coqc foo.v
coq coqtop
etc -> easy to implement but breaks backwards compat
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.
I guess when we change the binary names to rocq it could be a good opportunity to do this too
Yes, and the compatibility scripts / binaries could be small wrappers that call rocq.
Last updated: Oct 13 2024 at 01:02 UTC