incorporating std

Stream: lean4

[Paul Chisholm]

Now that std4 has been removed from the core lean4 build, what is the recommended way to incorporate std4 into a package created with lake.

[Mario Carneiro]

require std from git "https://github.com/leanprover/std4" @ "main"

in your lakefile

[Paul Chisholm]

Thanks, that works. Will this pick up changes to std4 on github during a subsequent build of my package, or do I have to manually delete lean_packages?

[Mario Carneiro]

Neither. The current commit you build against is kept in the manifest.json in your lean_packages (you should version control this file), and this file is updated when you run lake update but lake build just uses the version specified there

[Logan Murphy]

I've added the require clause to my lakefile as Mario suggested, and ran lake update and lake build.

Some imports work fine, like import Std.Data.List.Init.Lemmas, it works fine. But when I try to import Std.Data.List.Lemmas, for instance, I get

`/home/logan/.elan/toolchains/leanprover-lean4-nightly-2022-10-12/bin/lake print-paths Init Std.Data.Nat.Lemmas Std.Data.List.Basic Std.Data.Option.Lemmas Std.Classes.BEq` failed:

stderr:
info: Building Std.Tactic.NoMatch
error: > LEAN_PATH=./lean_packages/std/build/lib:./build/lib LD_LIBRARY_PATH=/home/logan/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/lib:./lean_packages/std/build/lib:./build/lib:./lean_packages/std/build/lib /home/logan/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/lean -DwarningAsError=true -Dlinter.missingDocs=true ./lean_packages/std/././Std/Tactic/NoMatch.lean -R ./lean_packages/std/./. -o ./lean_packages/std/build/lib/Std/Tactic/NoMatch.olean -i ./lean_packages/std/build/lib/Std/Tactic/NoMatch.ilean -c ./lean_packages/std/build/ir/Std/Tactic/NoMatch.c
error: stdout:
./lean_packages/std/././Std/Tactic/NoMatch.lean:36:20: error: unknown identifier 'isAtomicDiscr?'
./lean_packages/std/././Std/Tactic/NoMatch.lean:39:41: error: unknown free variable '_uniq.124'
./lean_packages/std/././Std/Tactic/NoMatch.lean:36:4: error: unknown free variable '_uniq.124'
error: external command `/home/logan/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/lean` exited with code 1

Any insight as to what I'm doing wrong?

[Mauricio Collares]

Probably mismatched toolchains? Std4 master is using leanprover/lean4:nightly-2022-10-09.

[Logan Murphy]

Ah yes, that fixed it. Thank you, Mauricio!