feat: save Format to db instead of rendered text

[david-christiansen]

This PR reworks the database layer to save pretty-printer documents, so clients can render them at any width. Additionally, information used by Verso, such as the identity of local variables, is saved.

TODO:

• Check for performance regression
• Compare output
• Check that it's enough for Verso

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 5d983cb against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.2T (+2.99%)
• mathlib-docs//maxrss: -4MiB (-0.07%)
• mathlib-docs//task-clock: +1m 19s (+0.60%)
• mathlib-docs//wall-clock: +11s (+2.55%)
• own-docs//instructions: +342.5G (+9.20%)
• own-docs//maxrss: +143MiB (+5.63%)
• own-docs//task-clock: +31s (+8.52%)
• own-docs//wall-clock: +8s (+4.80%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for efa5550 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.2T (+3.00%)
• mathlib-docs//maxrss: -4MiB (-0.06%)
• mathlib-docs//task-clock: +2m 16s (+1.02%)
• mathlib-docs//wall-clock: +13s (+2.89%)
• own-docs//instructions: +347.4G (+9.33%)
• own-docs//maxrss: +171MiB (+6.74%)
• own-docs//task-clock: +33s (+8.89%)
• own-docs//wall-clock: +9s (+4.96%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 97d8889 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.1T (+2.90%)
• mathlib-docs//maxrss: -3MiB (-0.04%)
• mathlib-docs//task-clock: +1m 28s (+0.66%)
• mathlib-docs//wall-clock: +10s (+2.26%)
• own-docs//instructions: +330.3G (+8.87%)
• own-docs//maxrss: +111MiB (+4.37%)
• own-docs//task-clock: +25s (+6.71%)
• own-docs//wall-clock: +7s (+3.99%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 8db927b against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.0T (+2.74%)
• mathlib-docs//maxrss: -4MiB (-0.07%)
• mathlib-docs//task-clock: +18s (+0.14%)
• mathlib-docs//wall-clock: +11s (+2.51%)
• own-docs//instructions: +317.9G (+8.54%)
• own-docs//maxrss: +78MiB (+3.07%)
• own-docs//task-clock: +28s (+7.60%)
• own-docs//wall-clock: +8s (+4.70%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for eb85cd0 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.0T (+2.75%)
• mathlib-docs//maxrss: -5MiB (-0.08%)
• mathlib-docs//task-clock: +44s (+0.33%)
• mathlib-docs//wall-clock: +8s (+1.87%)
• own-docs//instructions: +317.4G (+8.52%)
• own-docs//maxrss: +96MiB (+3.80%)
• own-docs//task-clock: +28s (+7.64%)
• own-docs//wall-clock: +7s (+4.21%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 3cc356e against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.0T (+2.76%)
• mathlib-docs//maxrss: -4MiB (-0.06%)
• mathlib-docs//task-clock: +51s (+0.38%)
• mathlib-docs//wall-clock: +11s (+2.52%)
• own-docs//instructions: +317.1G (+8.52%)
• own-docs//maxrss: +103MiB (+4.07%)
• own-docs//task-clock: +30s (+8.15%)
• own-docs//wall-clock: +9s (+5.08%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 71cc979 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.1T (+2.80%)
• mathlib-docs//maxrss: -5MiB (-0.08%)
• mathlib-docs//task-clock: +44s (+0.33%)
• mathlib-docs//wall-clock: +12s (+2.62%)
• own-docs//instructions: +318.3G (+8.55%)
• own-docs//maxrss: +125MiB (+4.91%)
• own-docs//task-clock: +30s (+8.00%)
• own-docs//wall-clock: +8s (+4.49%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 0377d76 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.0T (+2.76%)
• mathlib-docs//maxrss: -3MiB (-0.06%)
• mathlib-docs//task-clock: -1s (-0.01%)
• mathlib-docs//wall-clock: +10s (+2.18%)
• own-docs//instructions: +320.1G (+8.60%)
• own-docs//maxrss: +104MiB (+4.11%)
• own-docs//task-clock: +30s (+8.03%)
• own-docs//wall-clock: +8s (+4.80%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 0e02bf1 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.1T (+2.81%)
• mathlib-docs//maxrss: -4MiB (-0.06%)
• mathlib-docs//task-clock: +16s (+0.12%)
• mathlib-docs//wall-clock: +10s (+2.20%)
• own-docs//instructions: +318.9G (+8.57%)
• own-docs//maxrss: +112MiB (+4.40%)
• own-docs//task-clock: +28s (+7.63%)
• own-docs//wall-clock: +8s (+4.37%)

No significant changes detected.

[david-christiansen]

!bench

[leanprover-radar]

Benchmark results for 35a4c86 against 58b0f20 are in! @david-christiansen

• mathlib-docs//instructions: +2.0T (+2.76%)
• mathlib-docs//maxrss: -3MiB (-0.06%)
• mathlib-docs//task-clock: +33s (+0.25%)
• mathlib-docs//wall-clock: +10s (+2.35%)
• own-docs//instructions: +317.8G (+8.54%)
• own-docs//maxrss: +87MiB (+3.42%)
• own-docs//task-clock: +29s (+7.72%)
• own-docs//wall-clock: +6s (+3.63%)

No significant changes detected.