The documentation of the Instructions command from #17744 says https://github.com/coq/coq/blob/d52b7876c48f2b0c241acec1f7388ff7ac110470/doc/sphinx/proof-engine/vernacular-commands.rst?plain=1#L864-L869
According to my packaging logs, this doesn't seem to be quite accurate; usr/lib/ocaml/stublibs/dllcoqperf_stubs.so is installed only on x64 Linux, not on i386 systems. While I haven't checked that this makes Instructions non-functional, it seems quite likely (please correct me if this is not the case). I think either the documentation should be updated with this limitation, or the build/install should be fixed.
cc @rlepigre
The documentation of the
Instructionscommand from #17744 says https://github.com/coq/coq/blob/d52b7876c48f2b0c241acec1f7388ff7ac110470/doc/sphinx/proof-engine/vernacular-commands.rst?plain=1#L864-L869According to my packaging logs, this doesn't seem to be quite accurate;
usr/lib/ocaml/stublibs/dllcoqperf_stubs.sois installed only on x64 Linux, not on i386 systems. While I haven't checked that this makesInstructionsnon-functional, it seems quite likely (please correct me if this is not the case). I think either the documentation should be updated with this limitation, or the build/install should be fixed.cc @rlepigre