Zulip Chat Archive
Stream: mathlib4
Topic: how to use the mathlib cache?
David Renshaw (Feb 20 2023 at 21:56):
dwrensha@hafnium:~/src/mathlib4$ lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-02-10)
dwrensha@hafnium:~/src/mathlib4$ lake exec cache
error: unknown command 'exec'
Gabriel Ebner (Feb 20 2023 at 21:59):
It's lake exe cache get
Gabriel Ebner (Feb 20 2023 at 21:59):
No c.
David Renshaw (Feb 20 2023 at 22:02):
d'oh
David Renshaw (Feb 20 2023 at 22:02):
yep, that works for building mathlib4 itself
David Renshaw (Feb 20 2023 at 22:04):
but for my project that depends on mathlib4, i get:
$ lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4 to ./lake-packages/Mathlib
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: Building Cache.IO
info: Building Cache.Hashing
info: Compiling Cache.IO
info: Compiling Cache.Hashing
info: Building Cache.Requests
error: > LEAN_PATH=./build/lib:./lake-packages/Mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/home/dwrensha/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/lib:./lake-packages/Mathlib/build/lib /home/dwrensha/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/lean ./lake-packages/Mathlib/././Cache/Requests.lean -R ./lake-packages/Mathlib/./. -o ./lake-packages/Mathlib/build/lib/Cache/Requests.olean -i ./lake-packages/Mathlib/build/lib/Cache/Requests.ilean -c ./lake-packages/Mathlib/build/ir/Cache/Requests.c
error: stdout:
./lake-packages/Mathlib/././Cache/Requests.lean:7:0: error: no such file or directory (error code: 2)
file: lake-packages/mathlib/lakefile.lean
./lake-packages/Mathlib/././Cache/Requests.lean:13:2: error: unknown constant '_root_.String'
./lake-packages/Mathlib/././Cache/Requests.lean:12:4: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:15:5: error: unknown namespace 'System'
./lake-packages/Mathlib/././Cache/Requests.lean:22:43: error: function expected at
Option
term has type
?m.18
./lake-packages/Mathlib/././Cache/Requests.lean:22:43: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:22:60: error: function expected at
IO
term has type
?m.27
./lake-packages/Mathlib/././Cache/Requests.lean:22:60: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:23:2: error: unknown constant 'Pure.pure'
./lake-packages/Mathlib/././Cache/Requests.lean:23:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:23:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:24:20: error: expected command
./lake-packages/Mathlib/././Cache/Requests.lean:31:34: error: expected term
./lake-packages/Mathlib/././Cache/Requests.lean:38:17: error: expected term
./lake-packages/Mathlib/././Cache/Requests.lean:50:24: error: unknown identifier 'IO.HashMap'
./lake-packages/Mathlib/././Cache/Requests.lean:50:24: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:59:36: error: function expected at
Array
term has type
?m.73
./lake-packages/Mathlib/././Cache/Requests.lean:59:36: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:59:69: error: function expected at
IO
term has type
?m.89
./lake-packages/Mathlib/././Cache/Requests.lean:59:69: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:60:2: error: unknown constant 'Bind.bind'
./lake-packages/Mathlib/././Cache/Requests.lean:60:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:59:82: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:67:10: error: expected token
./lake-packages/Mathlib/././Cache/Requests.lean:84:28: error: expected token
./lake-packages/Mathlib/././Cache/Requests.lean:87:32: error: expected token
./lake-packages/Mathlib/././Cache/Requests.lean:97:22: error: unknown identifier 'IO.HashMap'
./lake-packages/Mathlib/././Cache/Requests.lean:97:22: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:99:26: error: expected token
./lake-packages/Mathlib/././Cache/Requests.lean:116:2: error: unknown constant 'PProd.mk'
./lake-packages/Mathlib/././Cache/Requests.lean:116:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:116:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:115:4: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:120:18: error: function expected at
IO
term has type
?m.286
./lake-packages/Mathlib/././Cache/Requests.lean:120:18: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:121:2: error: unknown identifier 'throw'
./lake-packages/Mathlib/././Cache/Requests.lean:121:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:121:8: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#synth', '/-!', '/--', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'example', 'export', 'gen_injective_theorems%', 'import', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mutual', 'namespace', 'noncomputable', 'notation', 'opaque', 'open', 'postfix', 'prefix', 'section', 'set_option', 'structure', 'syntax', 'theorem', 'universe', 'variable' or no space before spliced term
./lake-packages/Mathlib/././Cache/Requests.lean:124:2: error: unknown constant 'PProd.mk'
./lake-packages/Mathlib/././Cache/Requests.lean:124:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:124:2: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:123:4: error: unknown constant 'sorryAx'
./lake-packages/Mathlib/././Cache/Requests.lean:133:38: error: expected ':=', 'where', '|' or no space before spliced term
error: external command `/home/dwrensha/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/lean` exited with code 1
Arthur Paulino (Feb 20 2023 at 22:43):
Are you following https://github.com/leanprover-community/mathlib4#using-lake-exe-cache-on-your-project ?
David Renshaw (Feb 20 2023 at 22:50):
yeah, I think I'm following everything there
David Renshaw (Feb 20 2023 at 22:50):
Arthur Paulino (Feb 20 2023 at 22:57):
Ah, it seems like the folder name for the cloned mathlib4 repo has changed from mathlib to Mathlib
Arthur Paulino (Feb 20 2023 at 23:02):
No... it's because you've done require Mathlib ...
Arthur Paulino (Feb 20 2023 at 23:04):
Do require mathlib ... instead
Arthur Paulino (Feb 20 2023 at 23:07):
@Gabriel Ebner This is a fragile part of the code... it can break depending on how the user writes down the requirements
David Renshaw (Feb 20 2023 at 23:15):
that worked. Thanks!
David Renshaw (Feb 20 2023 at 23:15):
the readme says require mathlib4 from git
David Renshaw (Feb 20 2023 at 23:15):
I tried that too, and it didn't work
Arthur Paulino (Feb 20 2023 at 23:16):
It failed for the same reason
David Renshaw (Feb 20 2023 at 23:32):
I successfully set up my CI with this. Thanks! https://github.com/dwrensha/math-puzzles-in-lean4/actions/runs/4227821709/jobs/7342652316
Arthur Paulino (Feb 20 2023 at 23:40):
I included a fix for that in https://github.com/leanprover-community/mathlib4/pull/2403 (cc @Shreyas Srinivas). We better be coherent with what Lake does
Last updated: Dec 20 2023 at 11:08 UTC