Quick
index
main
eev
eepitch
maths
angg
blogme
dednat6
littlelangs
PURO
(C2,C3,C4,
 λ,ES,
 GA,MD,
 Caepro,
 textos,
 Chapa 1)
emacs
lua
(la)tex
maxima
 qdraw
git
lean4
agda
forth
squeak
icon
tcl
tikz
fvwm
debian
irc
contact
☿

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

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. Parsing diagrams


4. 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...!


5. Questions

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

  • (z,e) (2024sep20) Translating Martin-Löf's equality to low-level Lean
  • (z,e) (2024jul30) More detailed installation instructions for lean4-mode
  • (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?


6. 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")


7. 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.


8. "Oficina"

This is a proposal for a workshop - "oficina" in Portuguese - on Lean4, with very few prerequisites. Long story short: when I tried to learn Haskell I got stuck for years at certain specific points, and what got me unstuck was learning how to draw some kinds of "missing diagrams", in this sense. The same thing happened with me with Lean, and I want to check if these "missing diagrams" are useful to other people too.

Here is one of those diagrams: