Transition to ndjson export format

Main.lean

@@ -1,7 +1,26 @@
 import Export
 open Lean
 
-def semver := "2.0.0"
+def exportMetadata : Json :=
+  let leanMeta := Json.mkObj [
+    ("version", versionString),
+    ("githash", githash)
+  ]
+  let exporterMeta := Json.mkObj [
+    ("name", "lean4export"),
+    ("version", "3.0.0")
+  ]
+  let formatMeta := Json.mkObj [
+    ("version", "3.0.0")
+  ]
+
+  Json.mkObj [
+    ("meta", Json.mkObj [
+      ("exporter", exporterMeta),
+      ("lean", leanMeta),
+      ("format", formatMeta)
+    ])
+  ]
 
 def main (args : List String) : IO Unit := do
   initSearchPath (← findSysroot)
@@ -13,8 +32,8 @@ def main (args : List String) : IO Unit := do
     | some cs => cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!
     | none    => env.constants.toList.map Prod.fst |>.filter (!·.isInternal)
   M.run env do
-    modify (fun st => { st with exportUnsafe := opts.any (· == "--export-unsafe") })
-    IO.println semver
+    let _ ← initState env opts
+    IO.println exportMetadata.compress
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
-      let _ ← dumpConstant c
+      dumpConstant c

README.md

@@ -1,53 +1,29 @@
-A simple declaration exporter for Lean 4 using the [Lean 4 export format](https://ammkrn.github.io/type_checking_in_lean4/export_format.html)
+A simple declaration exporter for Lean 4 using the [Lean 4 NDJSON export format](./format_ndjson.md)
 
 ## How to Run
 
-```sh
-$ lake exe lean4export <mods> [options] [-- <decls>]
-```
-This exports the contents of the given Lean modules, looked up in the core library or `LEAN_PATH` (as e.g. initialized by an outer `lake env`) and their transitive dependencies.
-A specific list of declarations to be exported from these modules can be given after a separating `--`.
-The option `--export-unsafe` can be used to include unsafe declarations in the export file. This may be useful for testing and debugging other tools, where unsafe declarations can serve as negative examples.
-
-
-## Format Extensions
+1. Build lean4export with `lake build`
 
-The following commands have been added to represent new features of the Lean 4 type system.
+2. Call the `lean4export` binary with the correct lake env set up.
 
-```
-<eidx'> #EJ <nidx> <integer> <eidx>
-```
-A primitive projection of the `<integer>`-nth field of a value `<eidx>` of the record type `<nidx>`.
-Example: the primitive projection corresponding to `Prod.snd` of the innermost bound variable
-```
-1 #NS 0 Prod
-0 #EV 0
-1 #EJ 1 1 0
+```sh
+lake env <path to lean4export binary> <lean file without .lean suffix>+
 ```
 
+For example, let's assume we're working in the `mathlib4` directory, with the following structure: 
 ```
-<eidx'> #ELN <integer>
-<eidx'> #ELS <hexhex>*
-```
-Primitive literals of type `Nat` and `String` (encoded as a sequence of UTF-8 bytes in hexadecimal), respectively.
-Examples:
-```
-0 #ELN 1000000000000000
-1 #ELS 68 69  # "hi"
+|__ mathlib4 (*we are here)
+|__ lean4export
 ```
 
+We can invoke the exporter on the "top level" mathlib file and export mathlib with the following command:
+```sh
+lake env ../.lake/build/bin/lean4export Mathlib > out.ndjson
 ```
-<eidx'> #EZ <nidx> <eidx_1> <eidx_2> <eidx_3>
-```
-A binding `let <nidx> : <eidx_1> := <eidx_2>; <eidx_3>`.
-Already supported by the Lean 3 export format, but not documented.
-Example: the encoding of `let x : Nat := Nat.zero; x` is
-```
-1 #NS 0 x
-2 #NS 0 Nat
-0 #EC 2 
-3 #NS 2 zero
-1 #EC 3 
-2 #EV 0
-3 #EZ 1 0 1 2
-```
+This exports the contents of the given Lean module (here just the top level `Mathlib` module in the `Mathlib.lean` file), and its transitive dependencies. A specific list of declarations to be exported from these modules can be given after a separating `--`, and more than one module can be passed to the initial invocation by including more than one name (separted with a space).
+
+### Options
+
+The option `--export-unsafe` can be used to include unsafe declarations in the export file. This may be useful for testing and debugging other tools, where unsafe declarations can serve as negative examples.
+
+The option `--export-mdata"` can be used to include `Expr.mdata` items in the export file, which are removed by default as they should not have an effect on type checking.