General Programming

Stream: lean4

[Kevin Mullins]

I'm curious what the available resources are to learn the general programming side of Lean 4 atm. I do Haskell professionally so I'm really just looking for something that outlines everything language-specific briefly, not an introduction to pure FP itself.

[Tomas Skrivan]

Apart from the official documentation, there is also lean-4-hackers that might be a good introduction.

[Mac]

Thee is also the work-in-progress Functional Programming in Lean book which is intended to eventually be the official source for learning general programming in Lean. Unfortunately, only 1 chapter is finished so far.

[Arthur Paulino]

Not everyone likes this method but it's worked nicely for me: while the documentation for using Lean 4 as a general purpose FP language is still green, checking the Lean 4 source code is highly insightful

[Eric Taucher]

Arthur Paulino said:

checking the Lean 4 source code is highly insightful

Totally agree.

In another programming language after I started ignoring forums like StackOverflow and results from Google and instead found trusted repositories of regularly updated code (ref) and searched only those every time I needed to understand a method/function/predicate the quality of my code and the set of features used increased dramatically. Granted some example code is very hard to understand at fist but worth the effort.

The hardest part about this at the start was knowing which repositories to trust and which to avoid. After a year or more it was easy to know the excellent code from all of the others, even average code is not allowed into such list. :smile:

[Kevin Mullins]

Are there any like actual HTML rendered docs for the standard library and/or primitives?

[Henrik Böving]

Yes! https://leanprover-community.github.io/mathlib4_docs/ Linkable via: docs4#Nat

[Kevin Mullins]

Ah this is a good start.

[Kevin Mullins]

What's the idiomatic approach to dealing with non-terminating things? Like a cat implementation for instance only terminates when the input file is finite, or an interpreter for a Turing-complete language.

[Henrik Böving]

You can use a partial def which lifts the requirement for a termination proof, however it does also not allow you to use its definition from within a proof (that would break consistency). If you want to do loop based IO bound work we already have a partial def that can be used for this docs4#IO.iterate.

Note that Lean does still allow you to make arguments about things that do not terminate though. For example if you have a turing complete language you can specify its semantic via an inductive relation and do proofs on that.

[Kevin Mullins]

With this syntax https://leanprover.github.io/lean4/doc/do.html#returning-early-from-a-failed-match is there a way to handle the remaining cases individually?

[Chandan Sah]

how to download the " data " package?

[Chandan Sah]

I am getting following error saying " unknown package data"

[Chandan Sah]

image.png

[Mark Gerads]

It looks like you are trying to import something from mathlib. Are you sure that your lean project has a copy of mathlib?

[Henrik Böving]

He is trying to import something from mathlub3 in a Lean 4 project if he is posting here, that cannot work

[Chandan Sah]

Okey, I got that.

[Henrik Böving]

What tutorial are you following to write this? Do you really want to use Lean 4 or are you interested in mathematics with a solid library already doing most things for you, if that's the case you'll be better of with Lean 3

[Chandan Sah]

Yeah it seems lean 3 would be a better fit for me as I am just starting with the Automatic theorem proving.

[Chandan Sah]

image.png

[Chandan Sah]

I was following the instructions mentioned in this page. But on typing "Select Default Profile" on the command palette, these four options showed up, but GIT Bash did not show up. Can anyone tell why this might be happening? Because I feel I followed the instructions very carefully

[Chandan Sah]

image.png

[Chandan Sah]

@Henrik Böving

[Henrik Böving]

I'm afraid I don't know stuff about Windows or the Lean 3 setup, you will most likely have better luck in #new members or #general where the Lean 3 people hang out