importing file with `#exit` in

Stream: lean4

[Kevin Buzzard]

If foo.lean is just #exit and bar.lean imports foo then this generates an error (not a warning). Is there any way I can continue with my workflow of "porting several files line by line simultaneously and #exiting files in the middle so one can import another without errors"?

[Jireh Loreaux]

Comment out until the end of the file?

[James Gallicchio]

I wonder if you could make a command like stop for tactics, that consumes all commands after it in the file...

[James Gallicchio]

elab "#stop" command* : command => do
  return

is enough to consume all commands so long as they parse, but I'm not sure if you're dealing with type errors or parse errors

[Mario Carneiro]

If you set_option warningAsError false before #exit you should be able to import it