Should the opam package install the bytecode plugin?

coq-community / bignums

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

GNU Lesser General Public License v2.1

22 stars 22 forks source link

Should the opam package install the bytecode plugin? #56

Open MSoegtropIMC opened 3 years ago

MSoegtropIMC commented 3 years ago

I came into a situation where I want to run coqtop.byte in ocamldebug to analyze some runtime behavior. From those plugins which I use from the Coq Platform, the Bignums syntax plugin is the only one which does not install the bytecode plugin (.cmo) file. When I do a make byte; make install-byte for Bignums, I can run my code in coqtop.byte.

Since this the only missing basic plugin, I would suggest that the opam package also installs the bytecode plugin.

ejgallego commented 3 years ago

That's the correct thing to do indeed for opam packages.