Reckonlean

This hobby project is a Lean 4 implementation (and set of notes) for John Harrison's Handbook of Practical Logic and Automated Reasoning. This project is going on in conjunction with an internal functional programming in Lean 4 seminar following Functional Programming in Lean.

The original code accompanying Harrison's book is copyright (c) 2003-2007, John Harrison.

Setup

Install elan

Build the project. Currently it depends on std4 for some tactics, like #guard.

$ lake build

A full, cold build currently (6c2bec9) takes 1 min 50 seconds on an Ubuntu 22.03 t3.xlarge instance.

Run the proof and test scripts (adder_test, ramsey_test, prime_test, herbrand_test):

$ lake build adder_test
$ lake exe adder_test
...

$ lake build ramsey_test
$ ./build/bin/ramsey_test
...

If using VSCode and neovim extension, be sure to select --clean startup option or you get red and yellow squiggles everywhere that make development impossible.

See lakefile.lean for the set of proof and test scripts defined.

Upgrading Lean Version

1. update lean-toolchain to the desired version
2. blow away the manifest and .lake directory
3. lake build