mathlib no longer install on Windows

[dbonattoj]

Hi!

The command curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

do not work anymore, I think Mathlib removed the script and made a python package instead.

However, using their python package, the "update-mathlib" do not work anymore in the terminal either.

I guess the right command is now : leanproject upgrade-mathlib

However, this gives me an access error:

$ leanproject upgrade-mathlib

[WinError 5] access is denied: 'D:\\logical_verification_2019\\_target\\deps\\mathlib\\.git\\objects\\pack\\pack-83552742d32047ec99d7e1ea8fa9e3d1e6fbe285.idx'

Even if the terminal is open as administrator..

There seems to be no need anymore for leanpkg configure

So the only command to execute is: leanproject upgrade-mathlib which will download mathlib and configure it with the right commit.

followed by leanproject build instead of leanpkg build

However, leanproject build do not build:

$leanproject build
[...]
Command '['leanpkg', 'build']' returned non-zero exit status 1.

I redirected the output of leanproject build to a file leanproject build &> outbuild

Looking for the error:

$ grep "error" outbuild
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:1:0: error: file 'love02_tactical_proofs_exercise' not found in the LEAN_PATH
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:1:0: error: file 'love02_tactical_proofs_exercise' not found in the LEAN_PATH
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:1:0: error: file 'love05_inductive_predicates_demo_master' not found in the LEAN_PATH
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:3:0: error: invalid import: love02_tactical_proofs_exercise
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:3:0: error: invalid import: love02_tactical_proofs_exercise
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:3:0: error: invalid import: love05_inductive_predicates_demo_master
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:51:7: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:52:7: error: unknown identifier 'peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:53:7: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:55:17: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:55:35: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:62:7: error: unknown identifier 'peirce_of_em'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_sheet.lean:63:7: error: unknown identifier 'dn_of_peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:34:7: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:35:7: error: unknown identifier 'peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:36:7: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:38:17: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:38:35: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:56:7: error: unknown identifier 'peirce_of_em'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:57:7: error: unknown identifier 'dn_of_peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:60:22: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:60:40: error: unknown identifier 'peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:68:22: error: unknown identifier 'peirce'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:68:31: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:76:18: error: unknown identifier 'excluded_middle'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_homework_solution.lean:76:36: error: unknown identifier 'double_negation'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:122:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:96:2: error: unknown identifier 'mul_self_nonneg'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:166:0: error: code generation failed, VM does not have code for 'classical.choice'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:170:4: error: definition 'some_natural_number' is noncomputable, it depends on 'classical.choice'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:210:2: error: unknown identifier 'choose'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:210:9: error: unknown identifier 'z'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:210:11: error: unknown identifier 'h'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:210:13: error: invalid 'begin-end' expression, ',' expected
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:211:2: error: sync
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:146:2: error: unknown identifier 'mul_self_nonneg'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:219:7: error: unknown identifier 'btree'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:220:7: error: unknown identifier 'is_full'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:221:7: error: unknown identifier 'mirror'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:222:7: error: unknown identifier 'is_full_mirror'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:223:7: error: unknown identifier 'mirror_mirror'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:226:5: error: unknown identifier 'btree'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:226:16: error: unknown identifier 'is_full'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:238:17: error: unknown identifier 'is_full.empty'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:243:12: error: unknown identifier 'node'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:210:2: error: don't know how to synthesize placeholder
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:251:8: error: type mismatch at application
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:254:7: error: type mismatch at application
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:260:3: error: unknown identifier 'mirror'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:266:8: error: type mismatch at application
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:280:7: error: unknown identifier 'vector'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:271:2: error: invalid apply tactic, failed to unify
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:295:2: error: unknown identifier 'neg_neg'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:356:6: error: unknown identifier 'eq_of_add_eq_add_right'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:383:0: error: tactic failed, there are unsolved goals
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:396:6: error: ac_refl failed
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_sheet.lean:3:0: error: invalid import: love05_inductive_predicates_demo_master
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:3:0: error: invalid import: love05_inductive_predicates_demo_master
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_sheet.lean:57:0: error: invalid definition, '|' or ':=' expected
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_sheet.lean:54:49: error: function expected at
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_sheet.lean:54:49: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_demo.lean:416:2: error: simplify tactic failed to simplify
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:40:4: error: unknown identifier 'length'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:104:4: error: unknown identifier 'linarith'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:71:28: error: tactic failed, there are unsolved goals
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:104:4: error: don't know how to synthesize placeholder
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:207:8: error: unknown identifier 'use'
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:207:12: error: unknown identifier 'n''
D:\dev\logical_verification_2019\lean\love11_logical_foundations_of_mathematics_exercise_solution.lean:207:8: error: don't know how to synthesize placeholder
D:\dev\logical_verification_2019\lean\love05_inductive_predicates_homework_solution.lean:31:2: error: Invalid `case`: You gave 4 names, but the case introduces
D:\dev\logical_verification_2019\lean\love06_monads_homework_sheet.lean:32:0: error: invalid expression
D:\dev\logical_verification_2019\lean\love05_inductive_predicates_homework_sheet.lean:69:11: error: unknown identifier 'tc₃'
D:\dev\logical_verification_2019\lean\love05_inductive_predicates_homework_sheet.lean:70:2: error: unknown identifier 'tc₃'
D:\dev\logical_verification_2019\lean\love06_monads_homework_sheet.lean:32:0: error: command expected
D:\dev\logical_verification_2019\lean\love05_inductive_predicates_homework_solution.lean:45:2: error: Invalid `case`: You gave 4 names, but the case introduces
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:34:34: error: unknown identifier 'expr.repr'
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:38:0: error: _main: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:39:0: error: _main: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_homework_sheet.lean:55:0: error: LoVe.safe_intros: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:86:0: error: LoVe.intro_ands: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_homework_sheet.lean:100:0: error: LoVe.safe_destructs: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:111:0: error: LoVe.intro_ands: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:150:0: error: LoVe.destruct_ands: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:160:3: error: LoVe.destro_and: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:164:3: error: LoVe.destro_and: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:220:0: error: LoVe.list_constants: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_sheet.lean:221:0: error: LoVe.list_constants: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_solution.lean:190:2: error: type mismatch at application
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:104:20: error: invalid let-expression, term
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_solution.lean:195:3: error: LoVe.destro_and: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_exercise_solution.lean:199:3: error: LoVe.destro_and: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:120:14: error: invalid quoted symbol, failed to resolve it (solution: use `<identifier> to bypass name resolution)
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:120:8: error: don't know how to synthesize placeholder
except.map_error._sunfold
parser.decorate_error.equations._eqn_1
parser.decorate_errors._match_1.equations._eqn_1
except.map_error.equations._eqn_1
except.map_error.equations._eqn_2
parser.mk_error_msg
except.error.inj
linter.no_errors_found
tactic.trace_error
except.error.inj_arrow
native.float.round_error
tactic.retrieve_or_report_error
except.map_error._main.equations._eqn_2
parser.decorate_errors._match_1.equations._eqn_2
parser.decorate_errors
except.map_error._main
except.map_error._main.equations._eqn_1
parser.decorate_errors._match_1
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:196:3: error: exact tactic failed, type mismatch, given expression has type
except.error
parser.mk_error_msg.equations._eqn_1
parser.decorate_errors.equations._eqn_1
linter.errors_found
except.map_error
parser.decorate_error
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:217:2: error: type mismatch at application
tactic.decorate_error
except.error.sizeof_spec
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:232:3: error: LoVe.solve_with_name: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:243:3: error: LoVe.solve_with_name: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love07_metaprogramming_demo.lean:247:3: error: LoVe.solve_with_name: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love03_structured_proofs_and_proof_terms_demo.lean:12:0: error: type mismatch, term
D:\dev\logical_verification_2019\lean\love03_structured_proofs_and_proof_terms_demo.lean:16:9: error: invalid type ascription, term has type
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:70:0: error: LoVe.take: trying to evaluate sorry
D:\dev\logical_verification_2019\lean\love10_denotational_semantics_demo.lean:91:5: error: unknown identifier 'x'
D:\dev\logical_verification_2019\lean\love10_denotational_semantics_demo.lean:91:7: error: invalid expression starting at 91:4
D:\dev\logical_verification_2019\lean\love10_denotational_semantics_demo.lean:91:7: error: command expected
D:\dev\logical_verification_2019\lean\love10_denotational_semantics_demo.lean:95:0: error: type mismatch, term
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:92:6: error: non-exhaustive match, the following cases are missing:
D:\dev\logical_verification_2019\lean\love10_denotational_semantics_demo.lean:99:0: error: type mismatch, term
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:120:15: error: unknown identifier 'lam'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:123:0: error: invalid definition, '|' or ':=' expected
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:123:20: error: unknown identifier 'lam'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:148:17: error: unknown identifier 'map_tttree'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:166:2: error: unknown identifier 'map_tttree'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:166:19: error: unknown identifier 'map_tttree'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:166:17: error: don't know how to synthesize placeholder
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:177:2: error: unknown identifier 'map_tttree'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:177:19: error: unknown identifier 'map_tttree'
D:\dev\logical_verification_2019\lean\love04_functional_programming_exercise_sheet.lean:177:17: error: don't know how to synthesize placeholder
D:\dev\logical_verification_2019\lean\love13_rational_and_real_numbers_demo.lean:311:7: error: simplify tactic failed to simplify
D:\dev\logical_verification_2019\lean\love13_rational_and_real_numbers_demo.lean:338:2: error: linarith failed to find a contradiction
D:\dev\logical_verification_2019\lean\love09_hoare_logic_demo.lean:165:33: error: solve1 tactic failed, focused goal has not been solved
D:\dev\logical_verification_2019\lean\love06_monads_exercise_sheet.lean:167:3: error: invalid apply tactic, failed to unify
D:\dev\logical_verification_2019\lean\love06_monads_exercise_sheet.lean:189:6: error: invalid apply tactic, failed to unify
D:\dev\logical_verification_2019\lean\love09_hoare_logic_demo.lean:260:31: error: solve1 tactic failed, focused goal has not been solved
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_exercise_sheet.lean:74:0: error: invalid expression
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_exercise_sheet.lean:74:0: error: command expected
D:\dev\logical_verification_2019\lean\love12_basic_mathematical_structures_demo.lean:128:0: error: invalid structure value { ... }, field 'inv_zero' was not provided
D:\dev\logical_verification_2019\lean\love12_basic_mathematical_structures_demo.lean:128:0: error: invalid structure value { ... }, 'inv_mul_cancel' is not a field of structure 'field'
D:\dev\logical_verification_2019\lean\love02_tactical_proofs_exercise_solution.lean:189:2: error: match failed
D:\dev\logical_verification_2019\lean\love09_hoare_logic_exercise_solution.lean:83:61: error: solve1 tactic failed, focused goal has not been solved
D:\dev\logical_verification_2019\lean\love12_basic_mathematical_structures_exercise_sheet.lean:101:8: error: exact tactic failed, type mismatch, given expression has type

However, now I'm stuck :(

TL;DR: Windows install:

• Follow everything in Installing for windows but the "lean tools part":
  • Get Lean, Get Python, Configure Git, Install Lean Tools, Install and Configure the Editor
• In Install Our Logical Verification Repository Do commands:

  git clone https://github.com/blanchette/logical_verification_2019
  cd logical_verification_2019
  leanproject upgrade-mathlib
  leanproject build

The install seems to work now, but the build do not :(

Sorry for the long post, it was written organically while I was trying to solve the issue :)

Best regards :)

[blanchette]

I am sorry, I do not know who you are and I cannot provide support related to old instructions for a course that took place last year. Please go to the Zulip Leanprover chat for help on how to install Lean and mathlib. The procedure has changed quite a bit recently.

[dbonattoj]

Oh, that's a sad news, this repository and the associated text had a high visibility on internet around January, and it seems that the 2020 repository is not ready yet for show time.

If I happens to solve the issue I will post it here :)

Thanks anyway,

best regards,

Updated solution in : https://github.com/leanprover-community/mathlib-tools/issues/49

[blanchette]

Oh, that's a sad news, this repository and the associated text had a high visibility on internet around January, and it seems that the 2020 repository is not ready yet for show time.

I'm not sure what is your definition of show time. Indeed, we don't have installation instructions for 2020, but apart from that the lecture notes have been thoroughly updated and renamed, and widely publicized on the Internet around March by Kevin Buzzard. See

https://news.ycombinator.com/item?id=22794533

I strongly recommend you switch to the 2020 lecture notes, which are much better than the 2019 ones. :)

Jasmin