repeat'

Stream: lean4

[Scott Morrison]

Could repeat' in https://github.com/leanprover/std4/blob/main/Std/Tactic/Basic.lean#L95 be defined instead as

syntax "repeat'' " tacticSeq : tactic
macro_rules
  | `(tactic| repeat'' $seq) => `(tactic| all_goals (first | ($seq); all_goals repeat'' $seq | skip))

rather than having the repeat'Aux declaration?

[Mario Carneiro]

(first | tac | skip can be replaced by try tac btw)

[Mario Carneiro]

I believe the execution order is not exactly the same; repeat'Aux does a BFS order traversal and yours does DFS

[Mario Carneiro]

but the main reason I would prefer not to is because I don't like to use macros for control flow, it incurs the cost of running the tactic parser framework on every loop iteration

[Scott Morrison]

Great, I like the main reason. :-)

[Gabriel Ebner]

running the tactic parser framework on every loop iteration

This is not what happens at all. The parser is run only once. All the macro expansion happens on the Syntax level. Obviously don't use it for it tight loops, though I'd say the bigger issue there is term elaboration (repeat apply foo x is problematic not because repeat is implemented as a macro, but because foo x is elaborated in every iteration).

[Gabriel Ebner]

I think that macros are great for high-level control flow (where you could write the expanded tactics manually instead, just with more typing). Low-level control flow (like proof search etc.) should be done in MetaM.

[Mario Carneiro]

I'm fairly sure you could write tac such that repeat' tac calls a different version of repeat' on every iteration because tac is redefining it

[Mario Carneiro]

the parsing is only done once but the interpretation of the syntax object happens every time

[Mario Carneiro]

I would love it if tactics could be "partially evaluated" where given the syntax it produces an execution plan as a closure which is then applied to the tactic state

[Scott Morrison]

@Mario Carneiro, I left a comment on your repeat' commit to Std; probably easier to discuss here than on github.

[Scott Morrison]

I'd like to change repeat' so that if we hit the maxIters limit, all the remaining goals that haven't been tried yet are returned.

[Scott Morrison]

Without this it seems we'll lose goals (and this was happening to me in apply_rules when I switched to using repeat').

[Mario Carneiro]

pushed a fix

[Scott Morrison]

Thanks.

[Scott Morrison]

What is the correct method to bump Std (from mathlib4), given that our lakefile just points to the main branch?

[Scott Morrison]

I initially tried just removing lean_package and building again, but discovered that lean_package/manifest.json is actually checked into the repository, which surprised me.

[Mario Carneiro]

lake update updates the manifest