Keith Braithwaite

Stream: new members

[Keith Braithwaite]

Hi all,
I'm a software engineer who'd like to experiment with Lean, eventually as part of a round-trip workflow involving formal specification, automated testing, and LLM-generated code. To begin with, I want to learn some Lean by hand. I have followed the Mathematics in Lean tutorial far enough to have VS Code set up, the tools installed, and have worked through a few examples.

My target domain is not mathematical in that sense, and I'd like to able to explore Lean under my own power. Thus far I've found only tutorials which assume that I want to contribute to an existing project (in fact: Mathematics in Lean), or am following an academic course where some environment has been made available. I've not found what I'd really like, which is a tutorial or guide to starting a brand new Lean project with the command-line tools.

Functional Programming in Lean begins "It is best if you read this book with Lean open in your editor…" indeed yes. But, how do I get to that point?

What am I missing?

[Arthur Paulino]

https://lean-lang.org/install/

[Keith Braithwaite]

Thanks, but as I said, that I've done. I've been able to work through some examples in the Mathematics in Lean tutorial.

[Arthur Paulino]

Sorry, I (mis)read too fast.
To start a new project, use lake new ...

λ lake new --help
Create a Lean package in a new directory

USAGE:
  lake [+<lean-version>] new <name> [<template>][.<language>]

If you are using Lake through Elan (which is standard), you can create a
package with a specific Lean version via the `+` option.

The initial configuration and starter files are based on the template:

  std                   library and executable; default
  exe                   executable only
  lib                   library only
  math-lax              library only with a Mathlib dependency
  math                  library with Mathlib standards for linting and workflows

Templates can be suffixed with `.lean` or `.toml` to produce a Lean or TOML
version of the configuration file, respectively. The default is TOML.

[Keith Braithwaite]

Thanks!

[Keith Braithwaite]

And if I do that and put #eval 1+2 in a file as per Functional Programming's exercise 1.1 and the info view in VS Code says

error: workspace directory not found: .

what do I do to fix that?

[Kevin Buzzard]

Did you "open folder" in VS Code and open the root directory of the repository (with the lakefile.toml etc files in)?

[Keith Braithwaite]

Ah, no, I did not. VS Code noticed the new folder and opened it itself. I see that manually opening it has some side-effects.

[Keith Braithwaite]

OK, looks as if I'm in business! Thanks both.