fstar: gzip checked files

[mtzguido]

Add output_zipped_value as an analogue to output_value, which calls gzip
on the resulting marshaled string before writing to the channel. Idem
for input_value. Then use it to write compressed checked files.

This is not ideal, it would be better to just have a notion of a
compressed channel, but I couldn't find good support to do so in OCaml.
We could revisit it later, and perhaps use it to compress hint files
too.

The files reduce significantly, ~3x. Before

$ rm -f ulib/.cache/*.hints && du -ahx ulib/.cache/ | sort -h  | tail -n 20
1.4M	ulib/.cache/FStar.Pervasives.fsti.checked
1.6M	ulib/.cache/FStar.Math.Fermat.fst.checked
1.6M	ulib/.cache/FStar.Pervasives.fst.checked
1.6M	ulib/.cache/FStar.UInt128.fst.checked
1.7M	ulib/.cache/FStar.Pointer.Base.fsti.checked
1.7M	ulib/.cache/LowStar.Monotonic.Buffer.fsti.checked
1.8M	ulib/.cache/FStar.Seq.Properties.fst.checked
1.8M	ulib/.cache/FStar.Sequence.Base.fst.checked
1.8M	ulib/.cache/LowStar.BufferView.Down.fst.checked
1.9M	ulib/.cache/FStar.Matrix.fst.checked
1.9M	ulib/.cache/FStar.OrdSet.fst.checked
2.1M	ulib/.cache/LowStar.BufferView.fst.checked
2.2M	ulib/.cache/FStar.Buffer.fst.checked
3.0M	ulib/.cache/FStar.Pervasives.Native.fst.checked
3.2M	ulib/.cache/FStar.Tactics.CanonCommSemiring.fst.checked
3.7M	ulib/.cache/FStar.Reflection.Typing.fsti.checked
4.2M	ulib/.cache/FStar.Reflection.Typing.fst.checked
4.2M	ulib/.cache/LowStar.Monotonic.Buffer.fst.checked
4.7M	ulib/.cache/FStar.ModifiesGen.fst.checked
124M	ulib/.cache/

After:

$ rm -f ulib/.cache/*.hints && du -ahx ulib/.cache/ | sort -h  | tail -n 20
556K	ulib/.cache/FStar.UInt128.fst.checked
576K	ulib/.cache/FStar.Pointer.Base.fsti.checked
596K	ulib/.cache/LowStar.Monotonic.Buffer.fsti.checked
612K	ulib/.cache/FStar.Math.Lemmas.fst.checked
644K	ulib/.cache/FStar.Seq.Properties.fst.checked
652K	ulib/.cache/FStar.Sequence.Base.fst.checked
664K	ulib/.cache/FStar.Matrix.fst.checked
672K	ulib/.cache/LowStar.BufferView.fst.checked
688K	ulib/.cache/FStar.OrdSet.fst.checked
700K	ulib/.cache/FStar.Math.Fermat.fst.checked
732K	ulib/.cache/FStar.Pointer.Base.fst.hints
748K	ulib/.cache/FStar.ModifiesGen.fst.hints
772K	ulib/.cache/FStar.Buffer.fst.checked
812K	ulib/.cache/FStar.Pervasives.Native.fst.checked
1.1M	ulib/.cache/FStar.Reflection.Typing.fsti.checked
1.1M	ulib/.cache/FStar.Tactics.CanonCommSemiring.fst.checked
1.3M	ulib/.cache/FStar.Reflection.Typing.fst.checked
1.5M	ulib/.cache/LowStar.Monotonic.Buffer.fst.checked
1.6M	ulib/.cache/FStar.ModifiesGen.fst.checked
43M	ulib/.cache/

43M is about exactly what we get from making a compressed archive of all the old checked files together, which means we are not missing out too much out on repeated patterns or common structure (this won't be case for hints!).