mmj2 gives non-fatal error when starting up on iset.mm

[jkingdon]

When I start mmj2 on iset.mm, I get a dialog which says error in macro transformations and javax.script.ScriptException: TypeError: null has no such function "getSeq" in transformations.js at line number 96

If I add a dummy mathbox theorem, as at jkingdon iset-mathbox, then I get a similar dialog with:

Error in callback TRANSFORMATION_SET_UP:
null

In both cases, mmj2 seems to function normally after dismissing the dialog.

This is the checked in jar file from the master branch. When it starts up, it reports its version as Hi! I am mmj2 v2.5.1 as of 29-Dec-2016. I can run mmj2 on set.mm without these problems.

I would prefer that mmj2 just handle the lack of a mathbox theorem (or whatever the issue is here), as I think people are trying to run it on things other than set.mm or iset.mm, but if the right solution is for me to add a mathbox theorem or something else to iset.mm, please advise about what to add.

[david-a-wheeler]

Confirmed. I also get a non-fatal error on startup on version 2.4.1.

[jkingdon]

The E-UT-1504 Error in callback TRANSFORMATION_SET_UP: null symptom is still happening with iset.mm of 15 Aug 2018 (which now has a mathbox theorem), for whatever that is worth.

[ghost]

Hello @jkingdon,

I do not believe this will be hard to fix, except that the code is in javascript and I need to study up on that first :-) transformations.js is looking for getSeq.

There should be no problems if a .mm file has zero mathboxes. They are not part of the Metamath.pdf specification. That shouldn't be hard to fix because the transformations stuff is probably just looking to avoid inputting mathboxes as proof step justifications.

[Also, is transformations is running for no reason? Perhaps the startup parameters input via RunParms.txt can be changed? Are you not running mmj2 macros?]

I will investigate your other reported issues with Ubuntu installation also. Is Ubuntu super popular among mathematicians and logicians and / or students these days? Isn't there a "package" feature for Ubuntu -- wherein an app "package" is created?

[jkingdon]

My RunParms.txt looks like this:

LoadFile,/home/jkingdon/work/set.mm/iset.mm
VerifyProof,*
Parse,* 
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
RunProofAsstGUI

I don't know what most of that means except that if I change iset.mm to set.mm I don't get the warning. I don't know what mmj2 macros are.

At first I thought this warning was related to mathbox but that could be a red herring. I'm not sure it has much to do with it.

I'll respond to the Ubuntu question over at #10

[ghost]

@jkingdon -- I don't have a quick answer to making the code change or disabling transformations and macros. "macros" and "transformations" are javascript and various commands can be used simply by inserting a js command in a proof worksheet or via a RunParm. Exits have been installed at various places in the mmj2 code where commands can be invoked. It's a whole infrastructure for proof assistancy. automatically completing certain step sequences. Perhaps not well documented.

[digama0]

The idea is that things that are specific to set.mm are put in the js files, which can be hot-swapped by the user without recompiling mmj2. So the fact that they don't work on iset.mm is expected, although I haven't looked at exactly what part of it fails.

[ghost]

Hi @digama0 @jkingdon @david-a-wheeler -- Conclusion from my notes: make macros enabled = no the default.

SOLUTION? it appears that transformations.js in mmj2jar/macros
      tried to run a null callback routine. in line 96:

    var mathbox = getStmt("mathbox").getSeq();

      Apparently, if the input .mm file does not contain a theorem
      with label "mathbox", this code aborts on a null pointer.)

      SO...if there is no "mathbox", assume there are no mathboxes
      and therefore do not do mathbox stuff. Set the seqNo that
      the code wanted to some default? Like Integer.MAX_VALUE. 
      Or zero.

  SOOO...I made the following changes to 96* in transformations.js

// var mathbox = getStmt("mathbox").getSeq(); patch tempocat var mathboxStmt = getStmt("mathbox"); trManager.buildUWPProvers(assrtList, function(assrt) mathboxStmt != null && assrt.getSeq() < mathboxStmt.getSeq() && !badAssrtsRE.test(assrt.getLabel()) && !forbiddenAssrts.contains(assrt.getLabel()));

  The result was a failure of Null Pointer Exception in Provers.java
      at line 48 after being called by transformations.js at line 14:

E-UT-1504 Error in callback TRANSFORMATION_SET_UP: null at mmj.transforms.Provers$UseWhenPossible.(Provers.java:48) at jdk.nashorn.internal.scripts.Script$Recompilation$11$478AA$transformations.L:1#useWhenPossibleExt(transformations.js:14)

SOLUTION     On non-set.mm files use RunParms.txt with this line
    WORKAROUND:  at the beginning:

                 MacrosEnabled,no

                 Note that the current js, "Nashorn" has been 
                 deprecated in Java 11 and will be removed at a future
                 date. Also, perhaps as of now Mario is the only user
                 of macros. So perhaps make disabled the default.

[digama0]

I used Nashorn because it was the only script format that was supported on all Java 8 installations by default. You can actually change it to any other language supported by the user's java installation with the MacroLanguage RunParm. Here's my suggested fix for those lines:

var mathbox = getStmt("mathbox");
if (mathbox != null) mathbox = mathbox.getSeq();
trManager.buildUWPProvers(assrtList, function(assrt)
        (mathbox == null || assrt.getSeq() < mathbox) &&
        !badAssrtsRE.test(assrt.getLabel()) &&
        !forbiddenAssrts.contains(assrt.getLabel()));

I don't think it is best to have it disabled by default. I think most users use mmj2 to edit set.mm; probably jkingdon is an exception in this regard. One option is to have macros enabled by default iff the loaded file is called set.mm, but this isn't a foolproof method, and I suspect many users have renamed copies of set.mm on their machines for various reasons. Unfortunately there is no foolproof method for detecting when a mm file is set.mm or a fork thereof, but I am inclined to think that other databases are the exception not the norm.

Also, macros support more than just explicit macro calls via the $m statement in the worksheet and the RunMacro command; they are also run implicitly by the ! auto-steps for structure inference, type inference and congruence proofs, as well as arithmetic proofs if you ever do those. I think if you turn them off you will subtly decrease the quality of the unify command for users in a way that isn't obviously connected to a configuration option.

[ghost]

OK, super. I will add your code changes.

I appreciate what you're saying, and I grok it. Absolutely. Great.

Here is what I suggest: put in RunParms.txt as the first line:

disable macros if not using a set.mm database MacrosEnabled,yes

Then let's update transformations.js with your code fix and close this issue...

On Sep 26, 2018, at 17:51, Mario Carneiro notifications@github.com wrote:

I used Nashorn because it was the only script format that was supported on all Java 8 installations by default. You can actually change it to any other language supported by the user's java installation with the MacroLanguage RunParm. Here's my suggested fix for those lines:

var mathbox = getStmt("mathbox"); if (mathbox != null) mathbox = mathbox.getSeq(); trManager.buildUWPProvers(assrtList, function(assrt) (mathbox == null || assrt.getSeq() < mathbox) && !badAssrtsRE.test(assrt.getLabel()) && !forbiddenAssrts.contains(assrt.getLabel())); I don't think it is best to have it disabled by default. I think most users use mmj2 to edit set.mm; probably jkingdon is an exception in this regard. One option is to have macros enabled by default iff the loaded file is called set.mm, but this isn't a foolproof method, and I suspect many users have renamed copies of set.mm on their machines for various reasons. Unfortunately there is no foolproof method for detecting when a mm file is set.mm or a fork thereof, but I am inclined to think that other databases are the exception not the norm.

Also, macros support more than just explicit macro calls via the $m statement in the worksheet and the RunMacro command; they are also run implicitly by the ! auto-steps for structure inference, type inference and congruence proofs, as well as arithmetic proofs if you ever do those. I think if you turn them off you will subtly decrease the quality of the unify command for users in a way that isn't obviously connected to a configuration option.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/digama0/mmj2/issues/7#issuecomment-424918512, or mute the thread https://github.com/notifications/unsubscribe-auth/ApDxkcx1xtlKnrTIHuJI8Z1wJniGbDjBks5ufCESgaJpZM4R4TKK.

[david-a-wheeler]

As much as possible I would like mmj2 and its default configutation to just "automatically do the right thing". For example, I normally edit set.mm, but I have been known to edit iset.mm. Automatically doing the right thing is a goal, not a destination, but it is still a worthy destination.

[digama0]

I think that bug fixes like the one here in transformations.js should limit the issues even if you do open a non-set.mm database with macros on. Plus you may want to write your own macros or adapt the existing ones for other databases (in particular transformations.js which contains a large blacklist of theorems that you may want to add to or edit).

I think that adding that line to RunParms.txt makes sense.

[ghost]

well... the LoadFile,set.mm run parm is not automatic. so i want to put a comment there about run parm command MacrosEnabled,no.

with mario’s fix to transformations.js there will be a hard stop error message if using iset.mm for null pointer. that is ok if the user has a response.

i propose to apply these fixes to my patch-2 branch and mark this complete.

soooo...will someone running java 10 JRE be able to use this ?

.

On Sep 26, 2018, at 18:49, David A. Wheeler notifications@github.com wrote:

As much as possible I would like mmj2 and its default configutation to just "automatically do the right thing". For example, I normally edit set.mm, but I have been known to edit iset.mm. Automatically doing the right thing is a goal, not a destination, but it is still a worthy destination.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[ghost]

Fixes applied to https://github.com/ocatmetamath/mmj2/tree/ocatmetamath-patch-2

1. transformations.js handles non-presence of mathboxes now
2. E-UT-1504 Error in macro callback TRANSFORMATION SETUP -- I added the word "macro" so that a user would know it is macro related and could, in theory, update RunParms.txt
3. I added a "MacrosEnabled,yes" line before the LoadFile command along with the comment, "disable macros if not using a set.mm file". OK, so all macro-related mmj2 error messages contain the word "macro" now and if a problem arises, the user has recourse.

P.S. The V2.5.2.0926 mmj2.jar in my patch-2 branch is working pretty good now. Almost don't need to do any more testing :-) Except for some actual users trying the thing...

[digama0]

I looked into the Nashorn situation. It looks like GraalVM will be available by default beginning JDK 11, and it should not be difficult to convert the existing scripts to Graal (which is compatible with ECMAScript standards, unlike Nashorn). So probably we should do this if/when we upgrade compatibility to JDK 11.

[ghost]

By coincidence, I patched ProofAsst.java this morning to deal with non-set.mm files causing an exception. During the initTableAreas() or something. And I applied some difficult patches concerning Settings of TMFF, such as Format and Indent Nbr on the PA GUI Edit menu.

Regarding js, great news. Glad to hear it. OK.

On Oct 9, 2018, at 18:15, Mario Carneiro notifications@github.com wrote:

GraalVM

[jkingdon]

I am no longer seeing the null has no such function "getSeq" error with recent mmj2 (version of "mmj2 v2.5.3 as of 23-Sep-2019", using the mmj2.jar as checked in to git).