Zulip Chat Archive

Stream: std4

Topic: documentation efforts

Adrien Champion (Oct 18 2022 at 08:44):

I would be interested in contributing to std4 and I think (re-)writing documentation is a good place to start. We can discuss this during the mentoring sessions, but maybe mentors could point to places where better/additional doc would be useful

Adrien Champion (Oct 18 2022 at 08:45):

And/or have github issues with a doc tag so that we can close them when they're done

Adrien Champion (Oct 18 2022 at 17:29):

[ ] add top-level module doc, including main definitions, possibly implementation details, and search-engine-related tags

Adrien Champion (Oct 25 2022 at 14:16):

Regarding documentation efforts, maybe it would be a good idea to add doc-gen4 to the lakefile.lean, so that we can build and inspect the doc as we improve it.

Should I open an issue and PR this?

Adrien Champion (Oct 25 2022 at 14:19):

Actually, doc-gen4 (and std4 it seems) do not compile on macos M1, so maybe not

Henrik Böving (Oct 25 2022 at 15:41):

What's the errors?

Adrien Champion (Oct 25 2022 at 16:02):

Here are the std4 errors, with [...] to remove similar errors so that it abides by Zulip's character constraints

output

Linking runLinter
Building Std.Data.Nat.Lemmas
error: > /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -o ./build/bin/runLinter ./build/ir/scripts/runLinter.o ./build/ir/Std/Util/TermUnsafe.o ./build/ir/Std/Lean/NameMapAttribute.o ./build/ir/Std/Tactic/Lint/Basic.o ./build/ir/Std/Tactic/OpenPrivate.o ./build/ir/Std/Tactic/NoMatch.o ./build/ir/Std/Data/List/Init/Lemmas.o ./build/ir/Std/Data/Array/Init/Basic.o ./build/ir/Std/Data/Array/Basic.o ./build/ir/Std/Tactic/Lint/Misc.o ./build/ir/Std/Util/LibraryNote.o ./build/ir/Std/Tactic/Lint/Simp.o ./build/ir/Std/Tactic/Lint/Frontend.o ./build/ir/Std/Tactic/Lint.o -rdynamic
error: stderr:
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libleancpp.a(expr_eq_fn.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libleancpp.a(init.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libInit.a(Init.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libInit.a(Basic.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libInit.a(Prelude.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib/lean/libInit.a(QSort.o) has architecture arm64 which is incompatible with target architecture x86_64

[...]

ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: error: undefined symbol: _lean_inc_ref_cold

referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__1+0xba)
referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__1+0xae)
referenced by ./build/ir/scripts/runLinter.o:(symbol _lean_inc+0x1a)
referenced 2482 more times

ld64.lld: error: undefined symbol: _lean_alloc_small

referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__1+0x87)
referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__1+0x5e)
referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__2___rarg+0x87)
referenced 1462 more times

ld64.lld: error: undefined symbol: _lean_dec_ref_cold

referenced by ./build/ir/scripts/runLinter.o:(symbol _l_liftExcept___at_readJsonFile___spec__2___rarg___boxed+0x32)
referenced by ./build/ir/scripts/runLinter.o:(symbol _l_readJsonFile___rarg+0x37f)
referenced by ./build/ir/scripts/runLinter.o:(symbol _l_readJsonFile___rarg+0x36a)
referenced 3992 more times

[...]

ld64.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/bin/leanc exited with code 1
error: > LEAN_PATH=./build/lib DYLD_LIBRARY_PATH=/Users/adrien/.elan/toolchains/leanprover--lean4---nightly/lib:./build/lib /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/bin/lean -DwarningAsError=true -Dlinter.missingDocs=true ./././Std/Data/Nat/Lemmas.lean -R ././. -o ./build/lib/Std/Data/Nat/Lemmas.olean -i ./build/lib/Std/Data/Nat/Lemmas.ilean -c ./build/ir/Std/Data/Nat/Lemmas.c
error: stdout:
./././Std/Data/Nat/Lemmas.lean:152:42: error: no goals to be solved
./././Std/Data/Nat/Lemmas.lean:157:26: error: application type mismatch
Nat.le_antisymm h₁
argument
h₁
has type
a ≤ b : Prop
but is expected to have type
min a b ≤ min b a : Prop
./././Std/Data/Nat/Lemmas.lean:158:23: error: application type mismatch
not_or_intro h₁
argument
h₁
has type
a ≤ b : Prop
but is expected to have type
¬?m.8781 : Prop
./././Std/Data/Nat/Lemmas.lean:154:62: error: unsolved goals
case pos
a b : Nat
h₁ : ¬a ≤ b
h₂ : b ≤ a
⊢ min a b = min b a

case neg
a b : Nat
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ min a b = min b a
./././Std/Data/Nat/Lemmas.lean:162:25: error: application type mismatch
Nat.le_of_not_le h
argument
h
has type
a ≤ b : Prop
but is expected to have type
¬a ≤ min a b : Prop
./././Std/Data/Nat/Lemmas.lean:160:59: error: unsolved goals
case neg
a b : Nat
h : ¬a ≤ b
⊢ min a b ≤ a
./././Std/Data/Nat/Lemmas.lean:164:71: error: unsolved goals
a b : Nat
h : a ≤ b
⊢ min a b = a
./././Std/Data/Nat/Lemmas.lean:176:26: error: application type mismatch
Nat.le_antisymm h₂
argument
h₂
has type
b ≤ a : Prop
but is expected to have type
max a b ≤ max b a : Prop
./././Std/Data/Nat/Lemmas.lean:177:23: error: application type mismatch
not_or_intro h₁
argument
h₁
has type
a ≤ b : Prop
but is expected to have type
¬?m.10471 : Prop
./././Std/Data/Nat/Lemmas.lean:173:62: error: unsolved goals
case pos
a b : Nat
h₁ : ¬a ≤ b
h₂ : b ≤ a
⊢ max a b = max b a

case neg
a b : Nat
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ max a b = max b a
./././Std/Data/Nat/Lemmas.lean:179:72: error: unsolved goals
a b : Nat
h : a ≤ b
⊢ max a b = b
./././Std/Data/Nat/Lemmas.lean:187:32: error: tactic 'split' failed
x y : Nat
⊢ min (succ x) (succ y) = succ (min x y)
./././Std/Data/Nat/Lemmas.lean:190:12: error: tactic 'split' failed
n m : Nat
⊢ n - m = n - instMinNat.1 n m
error: external command /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/bin/lean exited with code 1

Adrien Champion (Oct 25 2022 at 17:48):

So this comes from running on macos M1, where Lean's linking fails. This causes failures on FFI, which Std4 does not have, but the linter is a default target and does trigger this problem

Adrien Champion (Oct 25 2022 at 18:35):

lake build Std works fine, as pointed out by Mac

Adrien Champion (Oct 26 2022 at 07:22):

Last updated: Dec 20 2023 at 11:08 UTC