how to install https://github.com/ammkrn/lean4export/ ?

Stream: general

[TongKe Xue]

Goal:

I'm trying to dump all of Lean & MathLib and see if it verifies under https://github.com/ammkrn/nanoda_lib

What I've figured out so far. I need

1. Create empty project, add to lakefile.toml:

[[require]]
name = "mathlib"
scope = "leanprover-community"

2. somehow install lean4export
3. run lake exe Lean4Export Lean ; lake exe Lean4Export MathLib

Basic Question: How do I install this custom lean4export from https://github.com/ammkrn/lean4export/tree/format2024 ? (Not seeing any Makefile, cargo.toml, CMake, ... ).

Thanks!

[Kim Morrison]

Can you explain why you are interested in that fork and that branch?

[TongKe Xue]

Happy to, let me know if there is flaw in logic / I should be using something else:

1. I am interested in testing out how well the Rust impl of the Lean Kernel works, namely https://github.com/ammkrn/nanoda_lib

2. Quoting the README of the nanoda_lib repo:

Export files can be created with lean4export. The format in the linked fork is expected by this type checker, and is under review for inclusion upstream. The link will be updated if/when the changes are merged.

My interpretation of the above is: nanoda_lib does not read "standard Lean4Export"; nanoda_lib reads a "slightly modified Lean4Export", pointed to by https://github.com/ammkrn/lean4export/tree/format2024

This is all guess work on my part, as I don't have an end to end working chain, so I don't know if all the intermediate logic is sound.

[TongKe Xue]

I'm now wondering if this code is broken

With regular 'lean4export', I can export Mathlib no problem (but output was only 2.7G, surprising as I read online it is supposed to be 8-10G)

With the ammkm lean4export, when I try to export Mathlib, I get an error of:

error: Export.lean:108:53: Application type mismatch: The argument
  e
has type
  Expr
but is expected to have type
  Bool → Expr
in the application
  if ck = true then e.updateLet! d v b else e
error: Export.lean:108:8: type mismatch, result value has type
  Bool × (Bool → Expr) × ?m.580
but is expected to have type
  Bool × Expr × ?m.485
error: Lean exited with code 1
Some required targets logged failures:
- Export
error: build failed

It is almost as if some Lean.Expr type got changed from 2024 until now, where some "Expr" became a "Bool -> Expr"

[TongKe Xue]

nanoda_lib]$ cargo run -- config_file
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.04s
     Running `target/debug/nanoda_bin config_file`

thread 'main' (107299) panicked at src/parser.rs:487:13:
export file declares unpermitted axiom "Lean.ofReduceNat"
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I think this basically works now; it runs for multiple seconds and then complains about unpermitted axiom; which seems to imply exporting + parsing is working

[Julian Berman]

I'm not in front of Lean at the moment but I'm pretty sure you no longer need the custom lean4export now with nanoda. The changes have been merged into the regular lean4export.

I'd suggest just installing that and trying it.

[TongKe Xue]

I'll add it to my todo list. At the moment, I'm already running nanoda_lib on the export of the Lean main library. (Slower than exporting). Waiting to see what it outputs.

[TongKe Xue]

cargo run -- config_file
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.04s
     Running `target/debug/nanoda_bin config_file`

thread 'main' (107505) panicked at src/tc.rs:797:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

hmm, this failed; I'm going to have to modify nanoda_lib so it prints out a bit more helpful msgs :-)

[TongKe Xue]

(I'm probably running nanoda_lib wrong); so far, nanoda_lib is slower than I expected.

I thought the low level kernel did not do much, and I expected it to run at maybe 10x or 100x the time of cat; i.e. a straight through linear reading of the file & some direct type checks.

[TongKe Xue]

I just tried using the leanprover/lean4export (instead of the ammk/lean4export).

Running nanoda_lib, it immediately fails an assertion:

cargo run --release -- config_file
    Finished `release` profile [optimized] target(s) in 0.03s
     Running `target/release/nanoda_bin config_file`

thread 'main' (138127) panicked at src/parser.rs:299:9:
assertion `left == right` failed
  left: (18610, true)
 right: (18597, false)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

(almost as it a parsing error & it misinterpreted the first things it parsed)