Can the 32-bit jsCoq target be cleaned up?

[artagnon]

Seems like old code.

[ejgallego]

To summarize the private discussion we had:

• when OCaml bytecode (no matter if 32 or 64 bits in origin) is compiled by jsoo max_int is 2^53-1
• if the OCaml code is independent of such matters, usually users are good
• however, in Coq we do something a bit more evil:
  • we run native coqc to generate .vo files (as the JSOO version is very slow)
  • we load these files with jsCoq

That's OK on 32bits (as the ints are wrapped), however it fails in 64 bits as the hashes of the files and other stuff will break due to coqc having a different integer size.

That requires us patching Coq, but it should not be a huge deal.

The remaining question is one of support; I assumed that using a 32-bit build would be "safer" in terms of trying to debug issues, imagine .vo loading fails, we can always use the 32-bit version and see if that's still the case. But thining a bit more about it I'm unsure that's really and advantage.

I was under the impression that js_of_ocaml was not supported on 64-bit toolchains, but I think I may be wrong, in the sense that JSOO is really its own arch.