Eev and Lean4

I am trying to learn Lean4. It's more fun than Agda. My messy notes about Lean are in lean.e.

Index:

• 1. LuaTreeLean
• 2. Animating type inferences
• 3. A problem with import
• 4. Questions
• 5. Adapting eev-rstdoc.el to Lean
• 6. Snippets

1. LuaTreeLean

This is an attempt to port my LuaTree thing from Maxima to Lean. Its git repository is here. Click on the screenshot below to enlarge.

2. Animating type inferences

The animated gif at the left below is my first attempt. See this thread, or click on the animated gif to go to the PDF with one frame per page. The screenshot at the right below shows how I edit these diagrams using an extension of Dednat6.

3. A problem with import

I am trying to learn how to split my programs into a "library" - let's suppose that it is called A.lean - and "tests", called, say, B.lean and C.lean. In theory I should just need a minimal Lakefile, like this one from LuaTreeLean, and a line like "import A" in the beginning of B.lean and C.lean, but apparently I am stumbling on bugs... in the test below - that is also here - the "import A" in B.lean works from "lake build" but not from "lean B.lean" or from Emacs:

• (eepitch-shell)
• (eepitch-kill)
• (eepitch-shell)
rm -Rfv /tmp/import-test/
mkdir   /tmp/import-test/
cd      /tmp/import-test/

cat > A.lean <<'%%%'
  def a := "42"
  #eval a
%%%
cat > B.lean <<'%%%'
  import A
  #eval a
  def main : IO Unit := IO.println s!"Hello {a}"
%%%
cat > lakefile.lean <<'%%%'
  import Lake
  open   Lake DSL
  package A
  @[default_target] lean_lib A
  @[default_target] lean_exe b { root := `B } 
%%%

 lake build            ;# ok
.lake/build/bin/b      ;# ok
lean A.lean            ;# ok
lean B.lean            ;# unknown package 'A'

find * .lake/ | sort

# (find-fline "/tmp/import-test/")
# (find-fline "/tmp/import-test/A.lean")
# (find-fline "/tmp/import-test/B.lean")

Click on the screenshot to enlarge. I asked a question about this in the Zulip Chat in this thread; TODO: explain why using /tmp/a.lean as a scratch file may be a bad idea, and how to fix LSP when it gets confused...!

4. Questions

Here are links to some of my questions on the Lean Zulip Chat:

• (z,e) (2024jun26) What parsers parses the "(ab : A×B)" in a "fun ... => ..."?
• (z,e) (2024jun22) Animating type inferences
• (z,e) (2024jun22) How does Lean "synthesize" a "get" inside a "do"?
• (z,e) (2024jun22) A minimal state monad?
• (z,e) (2024jun16) Elaborators for other syntax categories?
• (z,e) (2024jun15) "require from git" works in Emacs but not in the shell
• (z,e) (2024jun15) Introducing Partax, the Parser Compiler
• (z,e) (2024jun11) Is there a variant of repr that "prints the type"?
• (z,e) (2024jun09) Need help to debug an import - and maybe a lakefile
• (z,e) (2024jun09) Announcement: LuaTreeLean (not a question)
• (z,e) (2024jun07) Minimal setup for importing .lean files in the same directory
• (z,e) (2024jun03) run_cmd, monads, and tests for their methods
• (z,e) (2024jun01) "failed to synthesize instance ToLuaTree Name" inside "instance : ToLuaTree Name"
• (z,e) (2024may25) Tools for exploring data structures?
• (z,e) (2024may20) How do I translate Agda's "postulate" to Lean?
• (z,e) (2024may19) Where is this shorthand for match documented?
• (z,e) (2024may18) A command that prints the current namespace?
• (z,e) (2024may15) How do I write a "#check_syntax"?
• (z,e) (2024may13) leading_parser?
• (z,e) (2024apr28) Recommended ways to convert Lean4 code to LaTeX?
• (z,e) (2024mar11) IO.Process.output with stdin being a string?
• (z,e) (2023jun26) ~/.agda/defaults and ~/agda/libraries, but in Lean?

5. Adapting eev-rstdoc.el to Lean

(TODO: explain this!)

(find-lean4doc     "whatIsLean")
(find-fplean4doc   "getting-to-know/evaluating")
(find-leanmetadoc  "main/01_intro")
(find-leantpildoc  "introduction")
(find-leanmathsdoc "C02_Basics#calculating")
(find-leanrefdoc   "using_lean#using-lean-with-emacs")
(find-angg         ".emacs.lean.el")

6. Snippets

My notes on Lean are here: lean.e. They are indexed using anchors, are divided into e-script blocks, and most of these e-script blocks are made of a series of elisp hyperlinks - actually "shorter hyperlinks" - followed by a snippet, like this:

# (find-leanmetadoc  "main/02_overview")
# (find-leanmetadocr "main/02_overview.lean")
# (find-leanmetapage  9 "3 essential commands and their syntax sugars")
# (find-leanmetatext  9 "3 essential commands and their syntax sugars")
# (find-leanmetapage 11 "This image is not supposed")
# (find-leanmetatext 11 "This image is not supposed")
# (ee-copy-rest-3 nil "-- end" "/tmp/a.lean")

import Lean
open Lean Elab Command

elab "#withstring " x:str : command =>
  match x with
  | `("a") => logInfo x
  | `("b") => do { logInfo x; logInfo (repr x) }
  | `("c") => do { logInfo x; logInfo (repr x.raw) }
  | _ => Elab.throwUnsupportedSyntax

#withstring "a"
#withstring "b"
#withstring "c"

-- end

My htmlizer only htmlizes a few of these links. The links that end in "doc" and "docr" are implemented in elisp using eev-rstdoc.el - see this presentation - and the (undocumented) code in .emacs.lean.el; the links that end in "text" are explained here.