update Lean version and replace std to batteries
#150
Conversation
| @@ -12,7 +12,7 @@ lean_lib «lean4-metaprogramming-book» where | |||
| require mdgen from git | |||
| "https://github.com/Seasawher/mdgen" @ "v1.3.0" | |||
|
|
|||
| require std from git "https://github.com/leanprover/std4" @ "v4.7.0" | |||
| require "leanprover-community" / "batteries" @ git "main" | |||
There was a problem hiding this comment.
Shouldn't we use the corresponding tag -- i.e. https://github.com/leanprover-community/batteries/releases/tag/v4.15.0-rc1 -- so this doesn't break when Batteries updates its Lean version?
There was a problem hiding this comment.
Batteries updates will not break the code in this book until a lake update is manually performed.
This is not a problem, as any updates to Batteries should eventually be followed.
| @@ -386,7 +386,7 @@ elab "custom_assump_2" : tactic => | |||
| then return Option.some declExpr | |||
| else return Option.none | |||
| match option_matching_expr with | |||
| | some e => Lean.Elab.Tactic.closeMainGoal e | |||
| | some e => Lean.Elab.Tactic.closeMainGoal `custom_assump_2 e | |||
There was a problem hiding this comment.
I'm only scanning the PR so apologies for not trying to figure this out myself, but can you say something about what's happening here with the extra argument?
There was a problem hiding this comment.
The Lean.Elab.Tactic.closeMainGoal argument appears to have been increased. It now accepts the tactic name for use in error messages.
|
I think this looks mostly good to me, just left 2 minor comments. Appreciate the PR! |
|
Got it, ok thanks again! |
This book is very out of date.
This PR is the first step in an attempt to update this book.