Building binport

Stream: mathlib4

[Daniel Selsam]

Note: I will be traveling most of the next two weeks, and won't be able to re-run Binport if and when the lean4:nightly breaks compatibility. The pipeline is pretty involved, so I created a Dockerfile to serve as a reference: https://github.com/dselsam/mathport/blob/master/docker/Dockerfile

[Daniel Selsam]

Also, most of the cost in building mathport is building mathlib from scratch with all the exporting enabled, and for present purposes the mathlib exports only need to be updated after a relevant backport has been merged. I have started adding a PreData folder with all the mathlib+liquid exports to the release .tar.gz file, so new bin/syn-port outputs can be generated relatively easily (by rebasing mathport on top of lean4 and following the last few steps of the Dockerfile).