How to unit/doc test?

Stream: lean4

[James Good]

Hello,

I've only worked through a portion of the Functional Programming in Lean4 online book, but I did a google search to try and see how others may be unit/doc testing Lean4 code and the only thing that came up was this:
https://lean-lang.org/lean4/doc/dev/testing.html

Which seems to be a test suite which covers the code which implements Lean4.

I have no experience with C and have some intermediate knowledge of programming in Haskell in a non-professional capacity.

I know that one of the Haskell doctest libraries basically collects the code which is being tested in the docstring and sends it through the REPL to be executed, receives the stdout in a string and compares it to what the user expected to be the result in the docstring.

I've run lean -h to view all of the commands available to see if there might be an equivalent way to achieve this with lean, but that doesn't seem to be the case.

I also did a quick search on this zulip chat for "test" and "testing" before I posted this; nothing came up, hence I decided to create this post.

Any suggestions or help would be greatly appreciated!

[Henrik Böving]

You can use https://github.com/hargoniX/nest-unit for unit testing, tehre are plans to eventually integrate a proper testing framework with lake itself although I don't know about the progress on that.

[James Good]

Thank you, I'll check that out.

[Eric Rodriguez]

The FRO roadmap points to @Mac Malone as someone in charge of testing - how's the progress on this?

[Mac Malone]

The core test framework is still in the design phase, but completing it is one of the goals for this new year! Reservori and Lake have just been higher priority until cloud builds are finished.

[James Good]

Eric Rodriguez said:

The FRO roadmap points to Mac Malone as someone in charge of testing - how's the progress on this?

Wasn't aware of this roadmap. Looks great.

Lean is still way over my head at the moment with everything that's possible, and I'll need to slowly get myself acclimated. However, I will say that as someone who has programmed a bit in Rust, I can definitely see the influence regarding the tooling for getting started and setting up an initial project.

My first impression is rather positive, as the setup was seamless and easy to get a first hello world running and mess around with the language.

[David Thrane Christiansen]

For super simple doctest-like functionality, the #guard_msgs command in Std is quite nice. Try:

import Std

#guard_msgs in
#eval 1 + 1

Lean will complain, and offer a quick fix to insert the expected output for you.

[James Good]

David Thrane Christiansen said:

For super simple doctest-like functionality, the #guard_msgs command in Std is quite nice. Try:

import Std

#guard_msgs in
#eval 1 + 1

Lean will complain, and offer a quick fix to insert the expected output for you.

This definitely works, thank you. I tried it out in the online lean4 playground, but I haven't been able to import Std when I try on a project on my computer.

I took a look at the mathlib4 repo to get an idea of how requiring the std4 package from github works since I didn't see any instruction for how to do so in any of the official lean4 learning sources when I skimmed them.

First time I tried running lake update, I was receiving an error due to some new syntax that's used in the std4 lib's lakefile, which I was able to correct by running 'elan update'.

However, I ran into a final error which has stumped me; there's a red squiggle near where I attempt to import Std, and after some time of the vscode lean4 process doing some stuff in the background, it eventually fails with this error:

`/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lake setup-file /home/james/Desktop/dev/lean4_learning/fp_in_lean/FpInLean/Basic.lean Init Std` failed:

stderr:
info: [34/161] Building Std.Lean.CoreM
info: [35/162] Building Std.Tactic.RCases
info: [54/195] Building Std.Tactic.NormCast.Ext
info: [55/195] Building Std.Tactic.Case
info: [81/195] Building Std.Tactic.Lint.Misc
info: [85/195] Building Std.Tactic.TryThis
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Lean/CoreM.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Lean/CoreM.olean -i ./.lake/packages/std/.lake/build/lib/Std/Lean/CoreM.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Lean/CoreM.c
error: stdout:
./.lake/packages/std/././Std/Lean/CoreM.lean:48:22: error: invalid escape sequence
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Tactic/NormCast/Ext.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Tactic/NormCast/Ext.olean -i ./.lake/packages/std/.lake/build/lib/Std/Tactic/NormCast/Ext.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Tactic/NormCast/Ext.c
error: stdout:
./.lake/packages/std/././Std/Tactic/NormCast/Ext.lean:92:19: error: invalid escape sequence
./.lake/packages/std/././Std/Tactic/NormCast/Ext.lean:99:34: error: unexpected identifier; expected '['
./.lake/packages/std/././Std/Tactic/NormCast/Ext.lean:210:21: error: unexpected token 'for'; expected '['
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Tactic/Lint/Misc.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Tactic/Lint/Misc.olean -i ./.lake/packages/std/.lake/build/lib/Std/Tactic/Lint/Misc.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Tactic/Lint/Misc.c
error: stdout:
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:182:90: error: invalid escape sequence
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:185:63: error: unexpected token '.'; expected command
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:187:61: error: a universe level named 'level' has already been declared
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:187:66: error: unexpected token ')'; expected command
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:190:31: error: unexpected token '.'; expected command
./.lake/packages/std/././Std/Tactic/Lint/Misc.lean:190:85: error: unexpected token '`'; expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Tactic/Case.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Tactic/Case.olean -i ./.lake/packages/std/.lake/build/lib/Std/Tactic/Case.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Tactic/Case.c
error: stdout:
./.lake/packages/std/././Std/Tactic/Case.lean:129:17: error: invalid escape sequence
./.lake/packages/std/././Std/Tactic/Case.lean:190:56: error: application type mismatch
  evalCase __do_lift✝ ?m.33776 ?m.33879 ?m.33980 caseBody
argument
  caseBody
has type
  TSyntax `Std.Tactic.casePattTac : Type
but is expected to have type
  ST.Ref IO.RealWorld Term.State : Type
./.lake/packages/std/././Std/Tactic/Case.lean:190:13: error: invalid argument name 'close' for function 'Lean.Elab.Tactic.evalCase'
./.lake/packages/std/././Std/Tactic/Case.lean:190:49: error: application type mismatch
  evalCase __do_lift✝ ?m.33776 ?m.33879 patts?
argument
  patts?
has type
  Array (Option (TSyntax `term)) : Type
but is expected to have type
  Term.Context : Type
./.lake/packages/std/././Std/Tactic/Case.lean:194:57: error: application type mismatch
  evalCase __do_lift✝ ?m.37601 ?m.37704 ?m.37805 caseBody
argument
  caseBody
has type
  TSyntax `Std.Tactic.casePattTac : Type
but is expected to have type
  ST.Ref IO.RealWorld Term.State : Type
./.lake/packages/std/././Std/Tactic/Case.lean:194:13: error: invalid argument name 'close' for function 'Lean.Elab.Tactic.evalCase'
./.lake/packages/std/././Std/Tactic/Case.lean:194:50: error: application type mismatch
  evalCase __do_lift✝ ?m.37601 ?m.37704 patts?
argument
  patts?
has type
  Array (Option (TSyntax `term)) : Type
but is expected to have type
  Term.Context : Type
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Tactic/TryThis.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Tactic/TryThis.olean -i ./.lake/packages/std/.lake/build/lib/Std/Tactic/TryThis.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Tactic/TryThis.c
error: stdout:
./.lake/packages/std/././Std/Tactic/TryThis.lean:43:2: error: unknown attribute [widget_module]
./.lake/packages/std/././Std/Tactic/TryThis.lean:43:37: error: unknown identifier 'Widget.Module'
./.lake/packages/std/././Std/Tactic/TryThis.lean:356:4: error: unknown identifier 'Widget.savePanelWidgetInfo'
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/build/lib:/home/james/.elan/toolchains/leanprover--lean4---stable/lib/lean:/home/james/.elan/toolchains/leanprover--lean4---stable/lib:./.lake/packages/std/.lake/build/lib /home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean -Dlinter.missingDocs=true ./.lake/packages/std/././Std/Tactic/RCases.lean -R ./.lake/packages/std/./. -o ./.lake/packages/std/.lake/build/lib/Std/Tactic/RCases.olean -i ./.lake/packages/std/.lake/build/lib/Std/Tactic/RCases.ilean -c ./.lake/packages/std/.lake/build/ir/Std/Tactic/RCases.c
error: stdout:
./.lake/packages/std/././Std/Tactic/RCases.lean:716:39: error: invalid escape sequence
error: external command `/home/james/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1

[James Good]

(deleted)

[David Thrane Christiansen]

I suspect that this is an incompatibility between your Lean version and your Std version. Unfortunately, they're presently fairly tightly coupled, and there's no way for Std to declare ahead of time which versions of Lean it supports.

Try copying the lean-toolchain file from the Std repository and then type lake update in a terminal. This will generate a lock file (Lake manifest) that keeps Std at the version you want until you decide to update.

This will get easier in the future!