Add SetParser,mmj.verify.LRParser

[david-a-wheeler]

Enable adding additional check in mmj2 on definitions. Otherwise people can add definitions that are clearly nonsense, and since they are axioms, you can prove nonsense from them.

Per Mario:

It's a few seconds on set.mm, not so significant and certainly within CI tolerance. It's actually faster if you use preference storage (enabled by default), because it caches the grammar table after calculating it and only recalculates if the grammar hash changes. You need to add this line to the RunParms, before VerifyProof:

SetParser,mmj.verify.LRParser

[digama0]

I should mention that it wasn't really designed as a checker, it's mostly just for actual parsing. So I'm not sure if it works and gives errors in all the bad cases. I recommend testing it first with some bad databases to find out what happens (maybe the metamath-test repo?).

On Tue, Feb 12, 2019 at 9:11 AM David A. Wheeler notifications@github.com wrote:

Enable adding additional check in mmj2 on definitions. Otherwise people can add definitions that are clearly nonsense, and since they are axioms, you can prove nonsense from them.

Per Mario:

It's a few seconds on set.mm, not so significant and certainly within CI tolerance. It's actually faster if you use preference storage (enabled by default), because it caches the grammar table after calculating it and only recalculates if the grammar hash changes. You need to add this line to the RunParms, before VerifyProof:

SetParser,mmj.verify.LRParser

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/metamath/set.mm/issues/750, or mute the thread https://github.com/notifications/unsubscribe-auth/AA1A7Jx9BTr3yY_DysBfzBgVjI5jSi8gks5vMsuogaJpZM4a2fFK .

[david-a-wheeler]

I have no idea if it works in "all" cases, but it certainly DOES detect the otherwise-accepted sneaky definitions posted by saueran on 11-Feb-2019. And we can enable it right now with little extra time, so I don't see any downside to enabling it.

It certainly detects this:

$( This sneaky definition looks okay but is not. $)

  ${
    $( PLEASE PUT DESCRIPTION HERE. (Contributed by saueran, 11-Feb-2019.) $)
    wleftp $a wff ( ( ph ) $.
    $( PLEASE PUT DESCRIPTION HERE. (Contributed by saueran, 11-Feb-2019.) $)
    wbothp $a wff ( ph ) $.
    $( PLEASE PUT DESCRIPTION HERE. (Contributed by saueran, 11-Feb-2019.) $)
    df-leftp $a |- ( ( ( ph ) <-> -. ph ) $.
    $( PLEASE PUT DESCRIPTION HERE. (Contributed by saueran, 11-Feb-2019.) $)
    df-bothp $a |- ( ( ph ) <-> ph ) $.
    $( PLEASE PUT DESCRIPTION HERE. (Contributed by saueran, 11-Feb-2019.) $)
    anything $p |- ph $=
      ( wbothp wn wi wleftp df-leftp biimpi df-bothp mpbir mpbi simplim ax-mp
      ) ABZAMACZDZCZMOEZOCQAEZNDZRNAFGSHIOFJMNKLAHJ $.
  $}