search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

patch for missing transformation crash #49

Closed ishanpm closed 3 years ago

ishanpm commented 3 years ago

Hasty patch for #48. Just adds a nullity check for EquivalenceInfo.fillDeductRules()'s deduction rule detection.

digama0 commented 3 years ago

While this check should probably exist because a null pointer exception is not great, it seems pretty late in the process to be noticing the problem, and in #48 we've already disabled the module so we should bail much earlier (and without an error message, because nothing is wrong). I'm not super familiar with this code, so it's possible that dedCom should never be null assuming that it is initialized properly, but on your example database we should never have made it this far.

ishanpm commented 3 years ago

Looking further into it it looks like the NullPointerException only happens in the specific case where there is an implication operator with no equality deduction rules, because the entry for that operator in the hash table is never created. I changed that bit to populate all the tables in advance.

Strictly speaking, that makes the original code to add new table entries redundant, but a little defensive programming never hurt anyone: https://github.com/digama0/mmj2/blob/5f3badde8ba39a1f475706e314e6be4e99d286c0/src/mmj/transforms/EquivalenceInfo.java#L234-L238

This still does not fix the fact that ProofAsstUseAutotransformations,no,no,no should skip this entirely, but at least it won't crash.