One line Lean file (comments start new commands)

Stream: general

[Jason Rute]

This is a curiously valid one line Lean file:

import Mathlib /- -/ import Aesop /- -/ theorem foo : True := by trivial /- -/ #print axioms foo

Why does /- -/ allow starting a new command?

[Robin Arnez]

It's just whitespace

import Mathlib import Aesop theorem foo:True:=by trivial#printaxioms foo

works too

[Robin Arnez]

There is no requirement to have newlines between commands

[Jason Rute]

Oh, this is so ripe for abuse... :smiling_devil:

[Eric Wieser]

import Lean                                                                                                                                 run_cmd do Lean.logInfoAt (.atom (.original "".toSubstring ⟨330⟩ "".toSubstring ⟨335⟩) "#print") "'hooray' does not depend on any axioms" #exit

theorem hooray : False := by sorry

#print axioms hooray

[Jason Rute]

import Mathlib

lemma really_hard_lemma_with_long_proof (n : Nat) : n + n - n = n := by
  induction' n with n ih
  . simp
  . exact (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x = n + 1) (add_tsub_cancel_right (n + 1) (n + 1))) Nat.add_left_cancel_iff._simp_1) (eq_self 1))) set_option debug.skipKernelTC true lemma foo : ∀ (n : Nat), n + n - n = n := (fun n => of_eq_true (Eq.trans (congrArg (fun x => x = n) (add_tsub_cancel_right n n)) (eq_self n)))

lemma innocent_lemma [Add Nat] : 1 + 1 = 2 := by simp

theorem main_theorem : False := by
  have := @innocent_lemma ⟨fun _ _ => 0⟩
  simp only [instHAdd, OfNat.zero_ne_ofNat] at this

#print axioms main_theorem

[Aaron Liu]

Jason Rute said:

import Mathlib

lemma really_hard_lemma_with_long_proof (n : Nat) : n + n - n = n := by
  induction' n with n ih
  . simp
  . exact (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x = n + 1) (add_tsub_cancel_right (n + 1) (n + 1))) Nat.add_left_cancel_iff._simp_1) (eq_self 1)))/- -/set_option debug.skipKernelTC true/- -/lemma foo : ∀ (n : Nat), n + n - n = n := (fun n => of_eq_true (Eq.trans (congrArg (fun x => x = n) (add_tsub_cancel_right n n)) (eq_self n)))

lemma innocent_lemma [Add Nat] : 1 + 1 = 2 := by simp

theorem main_theorem : False := by
  have := @innocent_lemma ⟨fun _ _ => 0⟩
  simp only [instHAdd, OfNat.zero_ne_ofNat] at this

#print axioms main_theorem

you don't even need the comments you just need any whitespace

[Jason Rute]

Fixed

[Chris Henson]

Watch out, this is going to end up in the training data for future AI-generated Lean! :joy:

[Damiano Testa]

By the way, the commandStart linter checks that commands start on new lines: if you add set_option linter.style.commandStart true at the start of your files, the linter will complain.

[Arthur Paulino]

Maybe it should be true by default

[Damiano Testa]

It is true by default, but in mathlib, not in the online server.

[Arthur Paulino]

I mean, in the standard config of what the Lean toolchain has ootb

[Damiano Testa]

I also just realised that the linter only checks "commands after imports", so you can still go crazy with your imports.

[Damiano Testa]

Arthur Paulino said:

I mean, in the standard config of what the Lean toolchain has ootb

Ah, I did not think of this. The linter is a mathlib linter, not a lean one.

[Damiano Testa]

At least initially, some of the lean examples used indentation, if I remember correctly. Something like:

section A
  example : True := trivial
end A

So maybe the idea that commands should start at the beginning of a line is either not expected or should be interpreted up to whitespace.

[Jason Rute]

The linter doesn't seem to work, :smiling_devil:

import Mathlib
set_option linter.style.commandStart true

lemma really_hard_lemma_with_long_proof (n : Nat) : n + n - n = n := by
  induction' n with n ih
  . simp
  . exact (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x = n + 1) (add_tsub_cancel_right (n + 1) (n + 1))) Nat.add_left_cancel_iff._simp_1) (eq_self 1))) set_option linter.style.commandStart false set_option debug.skipKernelTC true lemma foo : ∀ (n : Nat), n + n - n = n := (fun n => of_eq_true (Eq.trans (congrArg (fun x => x = n) (add_tsub_cancel_right n n)) (eq_self n)))

lemma innocent_lemma [Add Nat] : 1 + 1 = 2 := by simp

theorem main_theorem : False := by
  have := @innocent_lemma ⟨fun _ _ => 0⟩
  simp only [instHAdd, OfNat.zero_ne_ofNat] at this

#print axioms main_theorem

[Henrik Böving]

Why is it even required to use the oddity that Lean allows multiple commands on the same line for this? You can just

def foo (x : Nat) := x
                                                                                                                                                                                                                                                                                                                                                                                                                -- evil code goes here
def other (x : Nat) := x

[Jason Rute]

It's more the oddity that commands don't have to start at the beginning on their own line. I mistakenly thought I needed to use comments to make this work, hence the thread.