Preprocessing DOM when running make

[yiyunliu]

Note that this pull request is not in an ideal shape to be merged just yet as it requires a node.js installation.

The problem that the PR addresses

coqdocjs.js now contains code that processes the html file when it's loaded by the web browser. However, these operations are quite slow for large files, especially foldProofs, which currently does two things:

• Find the body of the proofs and wrap them in an element with class proof
• Register event listeners so the proof element's visibility can be toggled

The first operation is quite slow. This file, for example, makes firefox hang for around 10 seconds before the page becomes responsive.

My solution

The good news is that the overhead of the first step can be done by preprocessing the html files produced by coqdoc when running make. That's exactly what this PR does.

I ported all the code that preprocesses the html file into a separate repository coqdocjs-static. The code from config.js and preprocess.js are pretty much copy/pasted from the coqdocjs.

The index.js script takes as an input the path to an html file and perform all operations from repairDom, replInTextNodes, foldProofs to the dom (except for the code that registers events) before printing the result to stdout (or overwrites the input file with the --inplace flag).

The static branch of my fork of coqdocjs includes coqdocjs-static as a submodule. The makefile calls index.js from coqdocjs-static on all generated html files. The coqdocjs.js is modified so it only registers events.

Benchmark

Here are the benchmark results of loading the fp_red.html file before and after the change.

Before:

After:

Todos

Ideally, I'd like to merge the code from the coqdocjs-static repo here and make the static generation a feature that is disabled by default, but can be optionally opted in if the input files are large. The static html generator requires a node.js and npm installation, whereas coqdocjs currently doesn't require any dependency at all.

I can probably do it with a few Makefile flags, but I don't know if there are a set of tests I can run to make sure nothing breaks.

UPDATE: I managed to add the static preprocessor in a (hopefully) backward compatible way, with the only downside being the introduction of ES6 modules, which can cause problems when browsing the files locally (see https://stackoverflow.com/questions/46992463/es6-module-support-in-chrome-62-chrome-canary-64-does-not-work-locally-cors-er?rq=1)

[yiyunliu]

Just want to add that this is the only javascript code that I've ever written so if anything looks wrong then it probably is :)

[liyishuai]

I can probably do it with a few Makefile flags, but I don't know if there are a set of tests I can run to make sure nothing breaks.

We don't have a test suite yet, so maybe good time to create a self-contained one under the /example directory.

[liyishuai]

and I suppose coqdocjs-static should be copied rather than linked before merging.

[yiyunliu]

I can probably do it with a few Makefile flags, but I don't know if there are a set of tests I can run to make sure nothing breaks.

We don't have a test suite yet, so maybe good time to create a self-contained one under the /example directory.

I can create an example. It would also be helpful if one of the maintainers can double-check that the output looks right.

and I suppose coqdocjs-static should be copied rather than linked before merging.

I have inlined coqdocjs-static in the latest commit. I moved the logic in coqdocjs.js that transforms the dom to a separate file called preprocess.js.

By default, coqdocjs.js imports and runs the preprocess function from preprocess.js. However, if the COQDOCJS_STATIC flag is set in the makefile, then the grep command removes the preprocess calls from coqdocjs.js as the work has been done. The expected behavior is that unless the COQDOCJS_STATIC flag is set, everything should behave the same as it did before the PR.

The only backward compatibility issue is the use of ES6 modules. To test the files locally, you must start a local web server or the browser will complain about CORS, although according to the information I can gather online, that's a somewhat reasonable behavior.

[yiyunliu]

I'm having second thoughts about using modules to split up the preprocessing logic because not being able to directly run firefox toc.html is quite annoying.

Perhaps we can use a perl or bash script to manually stitch the files together so we can still use the more lenient classic scripts?

[yiyunliu]

So I think a straightforward, backward-compatible solution could be structured like this:

• when the static flag is enabled, copy a minimal coqdocjs.js file that doesn't do any of the post-processing to the generated html directory.
• when the static flag is disabled, use a combination of unix commands or perl to combine the minimal coqdocjs.js, config.js, and preprocess.js into one big coqdocjs.js file that has the same behavior it does now.
• in the html header file, we load coqdocjs.js as a monolithic classic script. The user can browse local files without setting up a local web server, which is less secure but consistent with the old behavior

The only issue is that if the coqdocjs.js file would then be generated, which would make the COQDOCJS_LN flag awkward.

If it's considered too big of a change, I'd happily maintain my separate fork and pull from the upstream every once in a while. I don't think many people run into the same performance issue that I did, and it's probably not the best practice to have files with >3000LoC code anyways