Studying mathlib as a knowledge artifact; seeking "expor...

Stream: new members

[Stu B22]

Howdy folks, I have been looking at mathlib as a structured library of typed math concepts, from the knowledge management (KM) point of view. (I recognize that mathlib is an ongoing project, incomplete and imperfect, and that is just fine!)

I would like to look at the export.json file that is constructed as part of the doc-gen process for mathlib.
(That file is not the same as export_db.json.gz, which is a less-structured output from the next stage of the doc-gen process).
AFAIK I would need to install Lean and build mathlib before I could see export.json.
I have not tried to do the full Lean install yet.
I will enjoy doing so when I can, but if anyone can help me skip ahead to see export.json sooner, that would be swell.
I presume it appears somewhere in this neighborhood during a build of the mathlib docs:
/home/runner/work/doc-gen/doc-gen/mathlib/

Additional background on where I am coming from, including discussion of the "Mathematics Subject Classification" (MSC) taxonomy and recent work on math knowledge mgmt., in the mathlib channel of the Xena Discord:
May 23: https://discord.com/channels/679792285910827018/717708103059112007/846158094466547743
May 29: https://discord.com/channels/679792285910827018/717708103059112007/848263391458230353

[Bryan Gin-ge Chen]

I'm running doc-gen locally now and I can upload export.json later today when I'm back at the computer.

[Stu B22]

That's splendid Bryan, thank you very much!

[Stu B22]

Learned that "low level format" (aka export_format ex: lean --export=export.out --recursive) is a more faithful form of export for a given loadable fully-elaborated theory.
Discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20type.20checkers.20overview/near/240698222
leads us to https://github.com/leanprover/lean/blob/master/doc/export_format.md
"Lean can export .lean files in a low-level format that is easy to parse and process. The exported file contains only fully elaborated terms. The file describes hierarchical names, universe levels and expressions. These objects are used to declare inductive datatypes, definitions and axioms."
This lean low-level-format is suitable for external checking of the proofs by a typechecker like Trepplein
https://github.com/gebner/trepplein/blob/master/src/main/scala/trepplein/typechecker.scala
"Lean is an interactive theorem prover based on dependent type theory. For additional trust, Lean can export the generated proofs so that they can be independently verified. Trepplein is a tool that can check these exported proofs. Trepplein is written in Scala".

[Bryan Gin-ge Chen]

Here it is: export.json.zip (13 MB file, uncompresses to about 93 MB)

Note that it only takes about 10-15 minutes to generate, but I've been out and about until now.

[Stu B22]

Got it! I appreciate your time spent. This file should help me jump ahead in my learning.