Help on mmj2 start options

[Benoit]

Hi,

I'm having some trouble with mmj2: I always have to move the mm file I want to work on to the same directory as the MM program.  Is the directory of the mm file configurable ?

At startup, I see the output:

  [3] mmj2Path     =
  [4] metamathPath =
  [5] svcPath      =
  [1] runParmFile  =

If I understand correctly, they are respectively:

  the directory of the mmj2 program

  the directory of the metamath program AND of the mm file, which should be the same

  the directory of ??? (what does "svc" stand for ?)

  the runParms.txt file

Or maybe I should indicate the relative directory of the mm file with respect to that of the metamath program in the RunParms.txt file ?  E.g.

  LoadFile,../../git/set.mm/set.mm

Thanks,

Benoit

[Ishan Murphy]

From my experimentation, the mmj2Path is where it looks for the RunParams file, and the metamathPath is where it looks for the .mm file. The LoadFile command in the RunParams file can use a relative path; this will be relative to the metamathPath argument. If any of these arguments are blank, they will default to the current working directory. The actual Metamath program is completely unused by mmj2 as far as I can tell.

The easiest thing to do is to leave mmj2Path and metamathPath blank and just change the LoadFile command to point to the .mm file, relative to the directory with the .bat file you use to start mmj2 (an absolute path works fine too).

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/12cc87d3-de72-49da-b933-07f0d8a75746%40googlegroups.com.

[Jim Kingdon]

Editing LoadPath in RunParms.txt is how I did it.