docs for kernel type checking rules for Lean.Expr

Stream: general

[TongKe Xue]

LeanExpr refers to: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.Expr

Something inside:

• https://leanprover-community.github.io/lean4-metaprogramming-book/
• https://lean-lang.org/doc/reference/latest/

Is there a description of the "Lean Kernel Type Checking Rules" on Lean.Expr ? In the above two links, I am finding lots of related information, but not a concrete definition of what the "Lean Kernel" accepts and rejects in terms of Lean.Expr

Context:

1. I am playing with https://github.com/ammkrn/nanoda_lib
2. I have dumped all of the Lean module using the (nanoda_lib fork of) lean4export
3. I try to run nanoda_lib, with something like:

RUST_BACKTRACE=1 cargo run --release -- config_file

4. I get an error that looks like:
   PastedText.txt

5. nanoda_lib rejected something I exported from lean4export Lean

6. This is a bit weird -- but to figure out what is going on, I need to reference impl/description of what the Lean Kernel is supposed to do -- i.e. what it accepts/rejects.

Besides the C++ Lean4 Kernel source code, is there a description anywhere of what the Lean4 kernel is supposed to accept/reject? (I want to compare this to the nanoda_lib, and see where I screwed up the export process.)

Thanks!

[Henrik Böving]

#leantt is the formalization of the rules

[Henrik Böving]

(for Lean 3, modified slightly for Lean 4 as can be found in Sebastian Ullrich's PhD thesis)

[Chris Bailey]

There have been modifications to the kernel in the not so distant past, mostly changes to String.mk and string literals, as well as the addition of an eager reduction gadget with kernel support. The String changes are what's causing this particular error. The necessary changes were made to nanoda_lib in the debug branch when this issue was first noticed a few weeks ago.

The String changes haven't been merged into master yet, as I'm trying to get some time to finish sorting out this issue first; the head of mathlib has declarations that are not possible to export in the current version of the export format because the names coming from a library_note2 feature contain whitespace. When I get some time I'll move forward with the json format, then merge the type checker changes.

[Chris Bailey]

Also there's some prose/pseud-code info on type checking in this document: https://ammkrn.github.io/type_checking_in_lean4/title_page.html

[TongKe Xue]

1. Confirming that on nanoda_lib/debug branch, everything works fine:
   (this is type checking lean4export Lean)

RUST_BACKTRACE=1 cargo run --release -- config_file
   Compiling nanoda_lib v0.3.2 (/home/y/tt2/nanoda_lib)
    Finished `release` profile [optimized] target(s) in 11.19s
     Running `target/release/nanoda_bin config_file`
Checked 131241 declarations with no errors

output.txt

theorem Nat.add_zero (n : @Nat) : @Eq.{1} (@HAdd.hAdd.{0 0 0} n (@OfNat.ofNat.{0} 0)) n := @rfl.{1}

theorem Eq.symm.{u} :
  forall {α : Sort u} {a b : α}, @Eq.{u} a b → @Eq.{u} b a :=
  fun {α : Sort u} {a b : α} (h : @Eq.{u} a b) => @Eq.rec.{0 u} @rfl.{u} h

2. Could you point me at the docs/issue explaining why nanoda_lib does not use https://github.com/leanprover/lean4export and instead uses a fork? I.e. could this problem be solved by me writing some Rust code to parse the "official" lean4export ?

Thanks!

[Chris Bailey]

It doesn't require the use a fork anymore, the recommended additions were merged upstream. I updated the book but evidently not the README. Since it's not a live issue anymore I don't necessarily recommend reading the background, but for the record it's here.

[Chris Bailey]

Also these are the upstream changes of note:
https://github.com/leanprover/lean4/commit/cf8ffc28d306a9d8f442470b88f0385248e8cf32
https://github.com/leanprover/lean4/commit/cf871a892c2685af88baa76cdb134f4b980d9819
https://github.com/leanprover/lean4/commit/6e18afac8c3eda3b3a53006c67e6842cab2ac681

[TongKe Xue]

I failed to get https://github.com/leanprover/lean4export to work with nanolib/debug. Error:

git branch -v; RUST_BACKTRACE=1 cargo run --release -- config_file
* debug  e5438ac Test adjustment for String.mk redefinition
  master 66cca78 Add lifetime annotation to quiet new lint
    Finished `release` profile [optimized] target(s) in 0.03s
     Running `target/release/nanoda_bin config_file`

thread 'main' (154604) panicked at src/parser.rs:322:9:
assertion `left == right` failed
  left: (18610, true)
 right: (18597, false)
stack backtrace:
   0: __rustc::rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
   4: nanoda_lib::parser::Parser<R>::parse_expr_let_row
   5: nanoda_lib::util::Config::to_export_file
   6: nanoda_bin::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

This looks similar to the error I had yesterday, when trying leanprover/lean4export w/ nanoda_lib/master: #general > how to install https://github.com/ammkrn/lean4export/ ? @ 💬

Full commands I executed:

ExportProject]$ cat lakefile.lean
import Lake

open System Lake DSL

package ExportProject where version := v!"0.1.0"

require "leanprover-community" / mathlib

require lake4export from git
  "https://github.com/leanprover/lean4export" @ "master"
  -- "https://github.com/ammkrn/lean4export/" @ "master"



lean_lib ExportProject

@[default_target] lean_exe exportproject where root := `Main

then I used commands

25378  lake update
...
25383  lake exe lean4export Lean > nanoda_lean
25384  lake exe lean4export Mathlib > nanoda_mathlib

I'm trying to figure out what I'm doing wrong.

1. running wrong branch of nanoda_lib ?
2. running wrong version of leanprover/lean4export ?

[Chris Bailey]

See the previous comment about some mathlib declarations not being exportable in the current format. No branch of lean4export is currently capable of exporting mathlib properly, because library_note2 introduced declarations with names that the export format was not built to handle (from inception).

The white space handling in the debug branch is noted in the commit message as being "known incorrect"; I wanted to confirm that was indeed the issue. What's happening in your mathlib test is that two names that are the same except for different white space are being exported (improperly), and this improper export is not handled elegantly by the type checker. It's failing because a runtime check intended to prevent this kind of thing is doing its job.

Until the exporter is switched to use a format that can handle white space in identifiers, there is not a good way to export mathlib using lean4export. I don't have time to do it, but you're welcome to take a stab at implementing the JSON version as described in the GitHub issue.

[Chris Bailey]

If you're working on something specific, you can DM/email me about what you're trying to do and I'll see if I can point you in the right direction or help you find the right people to ask, if they don't show up here.