Enable using pa_j as a standalone camlp5r preprocessor

[aqjune-aws]

This patch enables using pa_j.cmo as a standalone camlp5 preprocessor.

For example, pa_j.cmo now can be used with camlp5r to preprocess a file 'test.ml' using the following command:

~/hol-light$ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo"   test.ml
    * HOL-Light syntax in effect *

File "test.ml", line 1, characters 8-15:
1 | let x = `1 + 2`;;
            ^^^^^^^
Error: Unbound value parse_term

This is necessary to support module compilation of HOL Light because this patch will enable preprocessing .ml files for compilation.

To achieve this,

• Printing "* HOL-Light syntax in effect *" is redirected to stderr, not stdout, because ocamlc was consuming the log from from stdout too.
• jrh_lexer is enabled by default.
• quotexpander is moved to pa_j.ml .
• bignum files had to be separately compiled without using pa_j because they were declaring modules which interfere with the preprocessor.

pa_j files for OCaml 4.xx were only updated because it was not clear how to support pa_j with OCaml 3. I was curious whether OCaml version 3 should be kept supported, however...

Checked that holtest.mk works with OCaml 4.14 + camlp5 8.03 and OCaml 4.05 + camlp5 7.10. The timeouts of a few tactics in miz3 had to be increased (probably due to its nondeterminism).

[aqjune-aws]

Updates in pa_j are motivated by https://github.com/monadius/hol-light/tree/native .

[jrh13]

I have verified on several platforms and OCaml versions that this appears to work, which is the main thing :-) It was quite tricky handling all that system stuff, thanks!

The miz3 update is orthogonal, but I think it's a good idea, since the use of explicit timeouts makes testing vulnerable to random variations - I've seen the same phenomenon.