search

isabelle-prover / proving-contest-backends

"proving-contest"-backends for several theorem provers
MIT License
12 stars 5 forks source link

Lean: fix bugs revealed by break the system competition #24

Closed kappelmann closed 5 years ago

kappelmann commented 5 years ago
  1. Fix axiom regex to correctly identify allowed axioms as abused here.
  2. Disable global notation restriction again because it can easily be outsmarted as done here

The only way I am aware to solve the global notation cheat is to

  1. Define the notation already in defs.lean
  2. Import defs.lean in check.lean BEFORE submission.lean so that the elaborator will fail in case of a notation cheat - see this Zulip discussion.
alexjbest commented 5 years ago

(as much as I want to "break the system" again next month, I think I've annoyed you too much already so I'll mention it now) I think

axiom «quot.sound : a» : false
theorem soundness_bug : false := «quot.sound : a»

still works even with this patch?

alexjbest commented 5 years ago

And now I am very confused, when I feed that input in even leanchecker looks like it gets confused and spits out just quot.sound : false? If that wasn't the case maybe ^axiom (.*?(?= :)) : [^:]*$ would work?

kappelmann commented 5 years ago

Uff, yes you are right Alex - the leanchecker only spits out quot.sound : false in this case, which makes it impossible to detect the cheat at this stage. I posted this for an open discussion on Zulip

kappelmann commented 5 years ago

Fixed this issue (:crossed_fingers:) by comparing the whole line containing an axiom. See here. Alternatively, one could use a different checker like trepplein (see Zulip discussion), but I had issues setting it up at first, and it requires more dependencies, like sbt. I am in favour in keeping the setup simple.

kappelmann commented 5 years ago

I also updated mathlib. @maxhaslbeck do not forget to merge before the competition.