macro hangs in NNG

Stream: new members

[Ben Laurie]

I'm doing the natural number game, and trying to define a macro makes it hang ... what's going on?

[Ben Laurie]

oops, guess that's not how to work this chat

[Johan Commelin]

Welcom @Ben Laurie, I tried to restore some order :wink:

[Ben Laurie]

thanks!

[Johan Commelin]

What do you mean with "trying to define a macro"? Could you please paste your code between #backticks ?

[Ben Laurie]

its 4/9 in algorithm world: macro "simp_add" : tactic => `(tactic|( simp only [add_assoc, add_left_comm, add_comm]))

[Ben Laurie]

oh, I see - I wasn't supposed to actually run that code myself, it was already defined

[Ben Laurie]

still don't understand why it hangs, though, but perhaps that will become clear later...

[Johan Commelin]

I wouldn't be surprised if NNG runs in some sort of sandbox where such macro's don't work properly.

[Richard Copley]

Ben Laurie said:

oh, I see - I wasn't supposed to actually run that code myself, it was already defined

That's right. The same question was asked here.
@Kevin Buzzard, that makes (at least) 3 :smile:

[Kevin Buzzard]

Please someone feel free to make a PR convincing people not to type that stuff into lean. Or shall I just delete the code completely? It plays no role in the game, I was just showing off how good I was at copy-pasting code I didn't understand when I wrote that level.