mmj2 bug fixing and testing plans

[ocatmetamath at icloud.com]

Hello mmj2 users,

I uploaded another set of patches to my branch off the mmj2 master,

ocatmetamath-patch-2.

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

The mmj2.jar file is, of course, accompanied by all of the source files :-)

And the source files contain comments at the beginning about what fixes were

applied.

Mostly I've patched the Proof Assistant Search facility, and I think glauco

would agree we are getting closer. But I definitely need someone else to test

this out because he is still experiencing non-responsive searches

occasionally. I was able to replicate his problems originally, but after my

patches I cannot.

I have also punched in a few fixes to problems resulting from entropy

(bitrot). Today Ctrl-F and Ctrl-B are working again in the PA GUI. And GMFF

export of the current proof worksheet in html and alt-htlm is working if your

proof contains the auto-complete character, "!", on any steps.

While I have the hood up I don't mind making fixes. So if anyone notices

anything that isn't in accordance with what seems correct, please send me an

email (along with data to replicate the problem, such as your proof worksheet,

your TL folder, if necessary, your runparms, and any sys print output from

Java or the command line (e.g. exceptions and dumps and messages...))

Then once glauco is squared away I am planning to set up batch tests of

Search, and also of the old (2011) batch regression tests. Perhaps using Ant,

or something else if research indicates a superior alternative. Anyone

interested in helping or leading, let me know. What would be ideal would be to

have a suite of tests to run on mmj2 to give a "thumbs up" with a certain

degress of confidence, say 99.9%, that new bugs didn't appear and that new

features do something approaching what they were promised as doing :-)

(Especially now that mmj2 has been forked down to Eclipse, and so many OS's

and platform levels of various versions.)

Naturally, once these fixes are tested I will send a pull request to Mario.

But only when the code is clean...

Thank you, 

Mel.

[Mario Carneiro]

I want to say that I'm glad you are back and working on mmj2 again. I think mmj2 is the best metamath IDE that currently exists, but I don't use all of its features, and I'm afraid to say the parts that I didn't use did not get much bugfixing love. If you can get the testing infrastructure working again, I will be a very happy person!

Mario

--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Glauco]

In my opinion, the search tool was awesome already :-)

In the last couple of years I've been using at least 10 times per day (on average)...

More generally, great IDE! (I got into the metamath world thanks to David's videos on mmj2; the Theorem Explorer is fascinating , but writing proofs was a bit intimidating...)

Glauco

[Jim Kingdon]

The mmj2: problem which I'm most aware of is https://github.com/digama0/mmj2/issues/7

There's java10 support, for which https://github.com/digama0/mmj2/pull/10 helped a bit but wasn't enough.

If I get the chance I'll try the ocatmetamath-patch-2 branch and see if the quirks I've been working around are still present.

[ocatmetamath at icloud.com]

Hi, here is some mmj2-related stuff from today.

1. It might be that someone has a PC that has 4MB of memory and wants to

conserve resources while working in mmj2. Aside from shutting down other

programs, there are RunParms.txt commands to use:

ProofAsstHighlightingEnabled,no

MacrosEnabled,no

DisableSettings

LoadProofs,No

* VerifyProof,*     gotta asterisk this out

A very retro start-up sequence, but if there is a problem in mmj2 then I might

ask you to re-try it with the first 3 commands so that we can isolate the

problem. (Those are beautiful enhancements, btw.)

2. Testing the Search Options in the latest ocatmetamath-patch-2 is good but

is incomplete, still. There are a ton of search options! One option in

particular is searching using parse trees, the "ParseStmt" and ParseExpr

formats. You can enter

$ap:Formulas:ParseStmt:>=:'-. ph'

and get every formula that is an instance of '-. ph'. And try this:

$ap:Formulas:ParseExpr:>=:'-. ph'

to find every sub-expression in set.mm of that form. That's pretty powerful

stuff. One question I have is why are Work Variables outlawed in the ForWhat

field. Is it just a concern about mmj2 taking the longest lunch break in the

history of the galaxy? Because I am sure that someone with a very densely

packed brain would want to do this. ToDo: research this.

3. Testing of Search Options: I having in mind adding a public "method"

(subroutine) to ProofAsst.java. It will have parameters includng Search Args,

input assertion list file name, output search results file name, and

Comment/Explanation. This will enable me to set up repeatable batch tests. It

will also be available as a powerful tool for extracting data. I think it will

be necessary to add one or two batch commands for testing. Once I have that

infrastructure in place I will be able to really fry my Intel Core I5 running

searches and rigorously testing mmj2 Search.

Any feedback, fire away. This is going to take a while so tell me if you

have any input (before I do the work.)

[ocatmetamath at icloud.com]

I fixed a gnarly bug today in the Search Results popup dialog (which

shows a single selection (assertion) in detail.) Fixed it in Step Selector

Search too. The problem was some mangling of the output showing

html tags and bad formatting. 

I also fixed a bug on Search Results and also Step Selector where

an accidental double-click of the right mouse button produced two

simultaneous results: an Apply of the selection to the proof step and

the popup dialog asking if you want to Apply. Now you can double

click the right-mouse button and not accidentally update your

Proof Worksheet (which, even with Undo is inconvenient and weird.)

You might have to right-mouse more than once. A little unresponsive,

which is my next todo. And also setting the dialog size automatically.

Couple things to iron out, but this is a big, big improvement, I think.

If anyone is not using the mmj2 "master" from github, I would be interested

in hearing from you about that. That is V2.5.1. Or perhaps you use 

the 2011 mmj2. That would be interesting. (It still works if the

proofs are in the old compression format or uncompressed.)

Try the ocatmetamath-patch-2 if you can. There may be cross-platform

incompatibilities -- and you may have useful feedback !

Thanks,

-mel.

[ocatmetamath at icloud.com]

OK, that is a fresh sample of the Search Results popup window (accessed via right-mouse 

click or right-double-click.) The Step Selector Search popup looks similar -- with normal looking

formulas and line spacing. 

Right now the popup size is fixed, but with long formulas and / or many hypotheses, scroll

bars are automatically inserted. What we're seeing is a JTextArea in a JScrollPane displayed

as the content of the JxxxDialogwhatever. Found that trick on the internet, and then 

stripped out the useless html tags but just for this popup window. So it all works now. Yay...

Another thing to note is that the Search Results windows displays the assertion 

comments, which the Step Selector windows do not. So, now that Search Options

and Search Results have improved appearance they also display the correct answers far

more often :-)  Almost trustworthy.

Finally, there may be differences in execution on different platforms and

computers. Mac/Unix/Windows are not 100% identical. More like 99.99% the same, perhaps.

So if you use mmj2 then please download the ocatmetamath-patch-2 mmj2.jar and

give it a bit of testing. I can provide a detailed list of the fixes and changes

if you don't want to wade through github.

==========================

[Glauco]

I've just tried the latest version and I'd like to emphasize that now I can easily copy/paste labels from the General Search Results window (which was one of my top wish list items...)

Nice job.

Glauco

[ocatmetamath at icloud.com]

Here is some information that may be useful -- to me if you review it and / or test the new code and 

tell me if I goofed...

1. I uploaded the change to set Syntax Highlighting off by default, for now. It is v2.5.2.1004.

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

That contains yesterday's refinement of the behavior of Settings, the new-ish feature

to save your session settings to disk and reload them automatically! And here is

some info about the topic, "Settings":

2. https://github.com/digama0/mmj2/issues/12#issuecomment-426876146

(I think that is a very clear and concise description. Some might say I am delusional

on that point.)

-mel

https://github.com/digama0/mmj2/issues/12#issuecomment-426876146

[Glauco]

I've noticed a couple of goodies (with recent mmj2 versions):

- when I launch mmj2, the latest .mmp I was working on is automatically loaded (I guess is part of the autosave setting behavior); other settings are saved also (for instance Set Soft Dj Vars Errors Handling, that I change back and forth often, for specific proofs)

I wish there was a menu option for Syntax Highlighting... :-)

- now, using single quotes, I can find specific labels: if you search for Cn you get a lot of results for pCnt also, but searching for  ' Cn ' nails down to what I was looking for

- I can use a bunch of single quote delimited search terms in a single line of the search windows, and those search strings are considered in AND condition (I don't know if this is in the documentation)

As expected, Metamath tools always get better; they never get worse...

Glauco

[ocatmetamath]

Yes. See the Help window. You can write 'OR' in between terms. The 'AND's are always implicit inside the ForWhat fields.

Concerning options. You can edit mmj2jar/store.json -- I disavow outcomes in that case -- and the File/Load Settings in PA GUI.

I am a little frustrated with store.json because it shows only non-default settings and I really want to be able to see everything. So that's like a bug :-)

I am actually still testing on settings now. I'm going to input every single batch command -- in one run if possible. I wonder if store.json can handle that. 

Thanks for the feedback. 

 

[Glauco]

Il giorno domenica 7 ottobre 2018 20:26:06 UTC+2, ocatmetamath ha scritto:

I am actually still testing on settings now. I'm going to input every single batch command -- in one run if possible. I wonder if store.json can handle that. 

Is there a fundamental reason why syntax highlighting cannot be toggled from the PA GUI? (if I'm not wrong, it can only be set on or off in the RunParms file, but you cannot change it without running a new mmj2 instance)

Glauco

[ocatmetamath]

yes

u cannot do it because it doesn’t work like that now.
especially now. i would debug it first.

[ocatmetamath]

At the moment I have several minor bugs in mmj2, such as the Theorem Loader

dialog boxes that ask for directories. And I noticed several RunParms that are

not using OS independent path separators -- so Windows vs. Mac means

doing battle with '/' and '\'. And I'm still trying to get the Settings file, store.json

to divulge all settings, not just the non-defaulted ones. And so it goes.

I am attaching a couple of files showing the directories and RunParmsTest.txt

that exercise almost every option and command via RunParms in a single

execution ... inside what I am calling "mmj2testbox". That is an isolated

environment for testing. I haven't finalized it but it is something that runs

and generates 40MB of output which can be file-compared to parallel runs

using older mmj2.jar files. I've collected mmj2v2011, mmj2v241, mmj2v252

and mmj2v252ocat.jar. So let the games begin!

[David A. Wheeler]

On Mon, 8 Oct 2018 08:46:55 -0700 (PDT), ocatmetamath <b252...@gmail.com> wrote:
> At the moment I have several minor bugs in mmj2, such as the Theorem Loader
> dialog boxes that ask for directories. And I noticed several RunParms that
> are
> not using OS independent path separators -- so Windows vs. Mac means
> doing battle with '/' and '\'.

That *may* not matter. If you're only passing the value to lower-level file opening APIs,
on Windows a "/" is treated just like a "\". There's only a problem if you pass the
path to a Windows command line like "dir" (where "/" is the option character).

> > While I have the hood up I don't mind making fixes. So if anyone notices
> > anything that isn't in accordance with what seems correct, please send me
> > an
> > email (along with data to replicate the problem, such as your proof
> > worksheet,
> > your TL folder, if necessary, your runparms, and any sys print output from
> > Java or the command line (e.g. exceptions and dumps and messages...))

Thank you SO MUCH for mmj2 in general, and for the recent fixes.

If I may: One of the biggest problems I have in mmj2's editor is matching parentheses.
If "matching parens" could be indicated in some way that'd be fantastic.

> > What would be ideal would
> > be to
> > have a suite of tests to run on mmj2 to give a "thumbs up" with a certain
> > degress of confidence, say 99.9%, that new bugs didn't appear and that new
> > features do something approaching what they were promised as doing :-)

It won't give you 99.9% right now, and it only has .mm format, but check this out:
https://github.com/david-a-wheeler/metamath-test

More tests to improve its coverage would be very welcome!

Ideally we'd measure coverage on several independent metamath processor
implementations, and then add tests to cover them all - that way, if an implementation
is missing a case but another one implements it, there will be very good odds that the
problem will be detected.

--- David A. Wheeler

[ocatmetamath]

Ok, thanks for the '/' heads up. Testing will reveal my error.

I am interested in your verifier test suite. It runs bash? and

it tests proof verification and .mm file syntax rules. Or just

proofs? I'm going to study it. Thank you for the info.

 

In mmj2\data\mm there are quite a few test .mm files with

various characteristics. Some strange ones. Help yourself.

I am considering how best to deal with automating tests.

bash was a  "problem dog" for me last time I tried to move

between Windows and Mac. So I scripted Python3 to run Python 3

and was happy. I will write down my ideas and see if they

sound good :-) Perhaps just discard. I don't have 10,000

hours to create something impossibly great. Just ok. Good

enough. Simple.

Regarding parentheses, I think we'll be exploring macros

much more in the future. Perhaps something to look at.

It is necessary to "up our game" because I understand

that Oracle will stop offering free Java 8 updates in 2019,

and our scripting engine may not be supported on

a different Java (what OpenJDK?)  See...with a macro

you could just type the command into the Proof 

Worksheet and hit Ctrl-U to find your paren or whatever.

So we ought to be able to deal with this .js stuff.

[David A. Wheeler]

On October 8, 2018 3:25:12 PM EDT, ocatmetamath <b252...@gmail.com> wrote:
>Ok, thanks for the '/' heads up. Testing will reveal my error.
>
>I am interested in your verifier test suite. It runs bash? and
>it tests proof verification and .mm file syntax rules. Or just
>proofs? I'm going to study it. Thank you for the info.

There are short sh scripts in it, but primarily it is a bunch of mm files to test whether or not a verifier reports verification correctly. In particular, it tries to test if a verifier except something that shouldn't accept, since rejecting shot something it should be accepting would be pretty quickly detected by current processes.

You can run a shell such as bash on Windows, one way to do it is cygwin.

>In mmj2\data\mm there are quite a few test .mm files with
>various characteristics. Some strange ones. Help yourself.

Cool. I have added that idea to the issue tracker.

>I am considering how best to deal with automating tests.
>bash was a "problem dog" for me last time I tried to move
>between Windows and Mac. So I scripted Python3 to run Python 3
>and was happy. I will write down my ideas and see if they
>sound good :-) Perhaps just discard. I don't have 10,000
>hours to create something impossibly great. Just ok. Good
>enough. Simple.
>
>Regarding parentheses, I think we'll be exploring macros
>much more in the future. Perhaps something to look at.
>It is necessary to "up our game" because I understand
>that Oracle will stop offering free Java 8 updates in 2019,
>and our scripting engine may not be supported on
>a different Java (what OpenJDK?) See...with a macro
>you could just type the command into the Proof
>Worksheet and hit Ctrl-U to find your paren or whatever.
>So we ought to be able to deal with this .js stuff.

I have not had time to track down the details of jdk licenses. I think there is no issue on Linux systems, because normally you just use the openjdk package on that Linux as provided by the linux distributor. The problem is Windows and Mac.


--- David A.Wheeler

[ocatmetamath]

I am attaching a file containing an mmj2 report, "The Grammar".

It is part of the output of RunParm

    PrintSyntaxDetails

Another command of possibly great interest is 

    PrintBookManagerSectionDetails,*

That last one is bigger than I want to upload here now since you can better 

run it yourself. And if you wish to store to a file you can put this RunParm in

    SystemOutputFile,sysoutSETUP.txt,new,""

You have to delete that print file before rerunning.

[ocatmetamath]

OK, I got the mmj2 Theorem Loader working. And while I am waiting for

my tests to complete allow me to explain this thing.

The "Theorem Loader" is unimaginatively named. It does what it is

called. When you complete a proof in the PA GUI you can load it

into the mmj2 Logical System and then begin working on another

proof that refers to it without exiting mmj2. And you can load it --

i.e. export it -- to disk in .mm format, complete with begin/end scope,

etc., ready for you to update into your .mm mathbox or whatever.

You can also, without exiting mmj2, use Theorem Loader to

load -- import -- an entire directory of .mmt (Theorem Loader)

files into the Logical System (one file per theorem.) 

There are a few fine points. the LOC_AFTER field on the PA GUI

comes into play with a new theorem -- you can tell mmj2 where

to insert the thing (the MObj < your theorem. But if your theorem

is new then the Theorem Loader inserts it based on its 

dependencies -- and the dependencies on other .mmt files

being loaded at the same time. 

There is a "formula as-is" option to let you update the formula

itself in the Logical System. Normally it just updates the proof

and $d's. 

So, later today maybe I'll upload this thing. I hope y'all play

with it. The ocat-metamath-patch-2 on github is identical to

Mario's "master" except for the fixes I have made (like a 30,000

mile auto servicing..but no detailing yet!)  If you do not

help test these fixes it just makes it a little harder for me. It

would be far better to have people on different OSes and

running OpenJDK and whatever to see if things work now.

Compile for yourself or try the mmj2.jar. 

[ocatmetamath]

P.S. re: Theorem Loader "nuances". 

On the TL menu you can set Proof Compression. But that controls, for some

reason, the PA GUI compression as well as the exported .mmt proof format.

But there is a catch: Normal and Compressed are the two standard formats

covered by the Metamath.pdf spec, whereas Packed is internal to mmj2

(as I understand it.) So...exported .mmt files do not show Packed, instead

they get compressed format, ready to insert in your .mm file. 

Also, there was a section of code involved with inserting Theorems 

and compressing proofs that converted severe validation errors into

"info messages" and nulls out the proofs. That never happens in real

life but in testing. It is also possible that "info messages" pass through

Travis whereas "A" or "E" types do not. I do not know, but I found the

start of code to add a 6th command line option, "testOption", and

I finished writing that code and then used it to recover the Theorem

insert error checking unless testOption = Y. (Do not use testOption

yourself, it has no value to you. I will use it later to add some

test diagnostics/test data capture code.) 

 Do not use it in real life. (Unless told to do

so, I suppose.) So we now can have our cake and eat it too. 

[David A. Wheeler]

On October 13, 2018 4:51:42 AM EDT, ocatmetamath <b252...@gmail.com> wrote:
>OK, I got the mmj2 Theorem Loader working.

Currently I use vim to edit the set.mm file to insert what I'm trying to prove. Then I start up mmj2 to load that file, tell it what I'm trying to prove, and prove it. Once I'm done I restart vim and I copy and paste the mmj2 results into set.mm.

Do your comments mean that I can do everything solely from within mmj2?


--- David A.Wheeler

[ocatmetamath]

Hmmmm....in theory you might not even have to go into the GUI,

just run batch commands. 

1. a new proof can be started in the PA GUI save File/Save Proof File

while incomplete: testX.mmp.  

2. a new proof can be started in a text editor as testX.mmt (or

testX.mmp since PA GUI proofs are text), and then and testX.mmt 

can be loaded via TL/Load Theorems From MMT Folder

3. When unification successful the proof can be stored in the

MMT Folder (typically mm2jar\myproofs) via 

TL/Unify + Store In LogSys and MMT Folder or

TL/Unify + Store In MMT Folder.

4. As a test, you can then TL/Load Theorems From MMT Folder

which imports to the Logical System after a little matter of

proof verification --> if fail pv then you get an empty proof

pls an error message. If good, then you ready for step 5.

 (THIS IS THE STEP BUGGING ME NOW

which has an issue with compressed proofs written to .mmt. and

why I need to debug more before the next upload.)

5. Manually edit set.mm and copy in text of testX.mmt -- 

here is where the need for a redo might be noticed when

you look at your new $d's and ask yourself... BTW, $d's

are written out to .mmt -- the .mmt format doesn't allow

for syntax or nested, shared scope between theorems,

so you gotta adjust in some cases (now. later perhaps

.mmt could perhaps generate $( comments containing

line numbers to update.

[ocatmetamath]

I think a “server mode” could easily be added.
Once mmj2 reads the RunParms.txt file it is closed
but it could await further commands...no gui...
just compute.

Then anything could happen — a pipe or a
front end / bridge that could be talking to other
processes.

Add to list.

[Glauco]

Hi Mel,

I use the TL a lot (and honestly, I don't consider it to be buggy at all).

I have 400 .mmp and .mmt files in a folder, and the .mmt files are loaded in the (how is it called, Logical System?) working area.

When a .mmp is complete, I TL > "Unify + store in MMT Folder"

Then I do go to the next .mmp file (create a new one or open a previously written partial proof), and then I do a TL > Load Theorems from MMT Folder. So it loads the new .mmt file in the working area.

It works like a charm.

But with my approach, it's hard to go back and change a .mmt file (for instance, change an Hypothesis). I would like to ask you if there's a way to "easily" manage the following two problems:

1) I've decided to drop an .mmt from the "working area": now I have delete it from the MMT folder and start a new mmj2 instance. Is there a way to "drop" an .mmt (and all its dependencies) from the "working area" without having to restart mmj2

2) assume that I decide to change an .mmt file: now I have to delete it and ALL the .mmt files that depend on it (recursively). If I run mmj2 and the "Load Theorems from MMT Folder" that runs at the beginning of the session doesn't find the proof for a label, mmj2 stops and I have to manually search all dependencies (and delete all the dependent .mmt files, recursively). Is there an option for "Load Theorems from MMT Folder" that loads all VALID proofs and automatically skips the proofs that (recursively) refer to a missing .mmt file?

Consider this example: I have th2.mmt that uses th1.mmt ; then I have 100 theorems that depend (possibly indirectly) on th2.mmt. Now I have to delete (and later recreate) all 102 .mmt files. But I only need to change th1.mmt and the "internal" proof of th2.mmt, all other 100 .mmt files don't need any change at all. If I was allowed to

- delete th1.mmt

- then if TL > "Load Theorems from MMT Folder" was able to automatically skip th2 (because th1 is not found) and all 100 theorems depending on th2 (maybe a warning that th1 is not found, would be cool)

I would then happily:

- open th1.mmp, change it and then store the new th1.mmt

- open th2.mmp, change it's proof using the new th1.mmt "signature" and then store the new th2.mmt

- then  TL > "Load Theorems from MMT Folder" and everything would be fine! (all other 100 theorems need not be recreated because th2's signature is unchanged)

Mel, is there an option (that I don't know of) to drop a theorem and all its dependencies from the "working area" (or for the "Load Theorems from MMT Folder" to recursively skip all .mmt files dependent on a missing .mmt?)

Thanks for your time

Glauco

[ocatmetamath]

<<I use the TL a lot (and honestly, I don't consider it to be buggy at all).>>

I assume you are running my latest version. so that's good to hear.

I'm willing to bet though, you're using ProofFormat = Normal,

because I *just* removed the restriction on Compressed TL

loads from the TL folder.

<<Consider this example: I have th2.mmt that uses th1.mmt ; then I have 100 theorems that depend (possibly indirectly) on th2.mmt. Now I have to delete (and later recreate) all 102 .mmt files. But I only need to change th1.mmt and the "internal" proof of th2.mmt, all other 100 .mmt files don't need any change at all. If I was allowed to

- delete th1.mmt

- then if TL > "Load Theorems from MMT Folder" was able to automatically skip th2 (because th1 is not found) and all 100 theorems depending on th2 (maybe a warning that th1 is not found, would be cool)

I would then happily:>>

Well, I *just* identified another section of code that generates messages

when updating the "Logical System" (that is just a name in mmj2  :-)

BUT the TL code has a commit/backout procedure so that in the

end the Logical System is in a consistent state and not destroyed.

So in TL, if there is a Proof Verify error, none of the updates will be

applied -- the first 99 theorems that were ok are reversed to the 

original state and you'll receive a message. 

Concerning your overall tasks, what would you think of

this: if TL creates a Metamath include file containing all

members of the TL folder that we're *just* loaded into

LogSys? I cannot easily do that without doing the update

because TL uses queues based on dependencies and

just stupidly follows orders -- but I can capture the flow

and output it to a file. Not today, but later maybe. I think

David A. Wheeler might find a use for that. (I like the

include file idea because if the file is goofy you can just

not include it -- and it provides a history/audit triail.) 

The include file would be in Metamath MObj.seq order

but it would not contain the LOC_AFTER to specify

an insert point, so they'd all go into the same

spot, the lowest possible spot.

P.S. I am going to fix the TL/Set MMT Folder dialog,

Use RunParms for now!

[ocatmetamath]

OK, the Theorem Loader (on my computer) is working with ProofFormat = Compressed.

It is hard to describe the good feelings when I started figuring it out...after spending 3

days battling Eclipse for control of my cursor! That software is neurotic! I would like

a dial on my keyboard so I could dial down on some things like that. 

And I made a great discovery while looking at my regression test. There is a bug

still, but it is in the mmj2 master as well, I believe. You can see it by unifying

"syllogism" or any other new (not already present) theorem you unify in mmj2,

regardless of Proof Format, but stipulating that it has logical hypotheses. 

I attach screenshot below.

What is great is that now I understand some of the comments about bouncing

between text editors and metamath.exe and mmj2. You couldn't start new

proof in mmj2 because of this bug. That is like an "anti-feature". So, when

I fix that, your experience will improve. For sure.

Also, I am convinced that I need to run that Theorem Loader batch test

"Unify + Store in LogSys and MMT" for every theorem. Probably take about

2 hours.

P.S. I noticed that Proof Unification in mmj2 PA GUI can take 5 seconds.

That is an expensive operation. I think it is in formatting of compressed

proof blocks. Are we sure we want those fancy compressed blocks (I

see the value and the beauty, I'm just asking.)

I may not upload any patches for a week. I have a lot of fixes now

and lots of testing. No reason uploading anything half-a$$ed because

your time is valuable (too). 

On Sunday, October 14, 2018 at 11:32:02 AM UTC-7, Glauco wrote:

[ocatmetamath]

here's the attachmnt:

[ocatmetamath]

<<Currently I use vim to edit the set.mm file to insert what I'm trying to prove. Then I start up mmj2 to load that file, tell it what I'm trying to prove, and prove it. Once I'm done I restart vim and I copy and paste the mmj2 results into set.mm. 

Do your comments mean that I can do everything solely from within mmj2? >>

Your method will change. Just enter text or paste into mmj2 PA GUI editor window

and work on proving. If not finished, save proof worksheet file -- the .mmp format --

and re-load it next time. When unification successful, then use Theorem Loader

to "Unify + Store in LogSys and MMT Folder". Thus you will have a .mmt file for

your theorem, which is actually just .mm format (and tell me if it can be more like

set.mm and I will update the formatting.) And your theorem is "in" mmj2, so you

can start another proof and refer to it. Then, next time you start mmj2 you can, if

you like, just Load Theorems From MMT Folder, and all the .mmt's will be inserted

into the Logical System -- and when you are satisfied with everything, then copy

the .mmt's into set.mm using something, like a text editor or a shell script :-)

Am attaching first insert after bug fix tonight. Yay...

[ocatmetamath]

P.S. And the end of that process is where I mentioned to glauco about creating

a composite file of all of the .mmt files in the MMT folder. They will be in insert/update

sequence, which is MObj.seq, or said differently, set.mm order -- which might save

you some time if there are many. You would just need to read that file and ... update

set.mm! (I do hope Metamath HQ always keeps an uncompressed version of the set.mm

platinum edition...just in case, keep the last few years...they zip down by 90%.)

[ocatmetamath]

OK, the me of two days ago was wrong, I uploaded to 

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

v2.5.2.1016 TL fixes + New Proof Bug

My testing todo list is getting so long I wanted to upload this so glauco 

and perhaps David can try the thing. (Remember: the TL Set Folder

dialog is fragile and will be worked on, so you can use it but quirkily.)

Email me if you find any bugs. 

Happy trails,

Mel L. O'Cat.

(hehe)

On Sunday, September 23, 2018 at 7:50:53 PM UTC-7, ocatmetamath wrote:

Hello mmj2 users,

I uploaded another set of patches to my branch off the mmj2 master,

ocatmetamath-patch-2.

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

The mmj2.jar file is, of course, accompanied by all of the source files :-)

And the source files contain comments at the beginning about what fixes were

applied.

Mostly I've patched the Proof Assistant Search facility, and I think glauco

would agree we are getting closer. But I definitely need someone else to test

this out because he is still experiencing non-responsive searches

occasionally. I was able to replicate his problems originally, but after my

patches I cannot.

I have also punched in a few fixes to problems resulting from entropy

(bitrot). Today Ctrl-F and Ctrl-B are working again in the PA GUI. And GMFF

export of the current proof worksheet in html and alt-htlm is working if your

proof contains the auto-complete character, "!", on any steps.

While I have the hood up I don't mind making fixes. So if anyone notices

anything that isn't in accordance with what seems correct, please send me an

email (along with data to replicate the problem, such as your proof worksheet,

your TL folder, if necessary, your runparms, and any sys print output from

Java or the command line (e.g. exceptions and dumps and messages...))

Then once glauco is squared away I am planning to set up batch tests of

Search, and also of the old (2011) batch regression tests. Perhaps using Ant,

or something else if research indicates a superior alternative. Anyone

interested in helping or leading, let me know. What would be ideal would be to

have a suite of tests to run on mmj2 to give a "thumbs up" with a certain

degress of confidence, say 99.9%, that new bugs didn't appear and that new

features do something approaching what they were promised as doing :-)

[ocatmetamath]

Glauco has discovered a bug in the latest, v2.5.2.1016 mmj2.jar version.

Here is what I just wrote back to him -- since the info is potentially helpful,

I repeat it here:

You're doing right. Loading at startup is fine, normally.

The bug in mmj2 now: if the .mmt theorem does not

already exist in set.mm and if it has zero logical hypotheses

then mmj2 has a load error (bug). 

I proved this by manually cut-n-pasting dvmptconst.mmt

into set.mm and then pulling it up in the PA GUI. I then

did Unify+Store in LogSys and MMT, and then after

that the regular Load Theorems From MMT Folder worked

fine. QED: the normal mmj2 .mm file load is operating differently

than the mmj2 TL .mmt load. 

For now I would just say to use Proof Format = Normal

if you are relying on Theorem Loader. I expect this bug

to be fixed in a day or two, but until then don't use

compressed proofs with Theorem Loader. 

Secondly, I would suggest to always keep your .mmp

Proof Worksheets that match the .mmt files. The

.mmp's re-generate the RPN proofs using unification,

whereas an input .mm or .mmt file directly reads the

RPNs, compressed or not, and tries to rebuild the

proof steps. So there is a safety factor in having the

.mmp's. 

The good news is that I ran a batch test last night

of the entire set.mm of Sep 4 using this command:

UnifyPlusStoreInLogSysAndMMTFolder,99999,,Print

That executed the TL UnifyPlusStoreInLogSysAndMMTFolder

for every theorem except dummylink. All passed the

test, which is a considerable test of reading a theorem,

creating a proof worksheet, unifying it, creating a .mmt

file for it, and then loading that .mmt update back into

the PA GUI Logical System and the MMT Folder while

also printing the proof worksheet to a sysprint file.

Took about 15 minutes. Interestingly, error message

appeared for a number of theorems that are like

dummylink: idi, natded, conventions, iin1, iin2 and iin3.

The error message alarmed me but mmj2 does not

and never has been able to process proofs consisting

of nothing but variable hypotheses. So, mmj2 kicks

out a message and we ignore it? OK with me for now.

Another interesting thing: that command allows for an

input file -- just like the ProofAsstBatchTest command:

UnifyPlusStoreInLogSysAndMMTFolder,99999,extracted-proof-worksheets.mmp,Print

It can read the entire set.mm from a file of .mmp's

and go through the test. You could use a file like

that instead of a folder of .mmt's.

* * *

So, westward ho. Progress must be made.

[ocatmetamath]

I just uploaded v2.5.2.1017 which fixes this morning's bug from glauco

(a simple matter of my overlooking the other pathway into the Logical

System --> no compressed proof block input, turn right.)

I updated the main TL batch command but have not tested iit with

an input file yet, just with the default of reading the Logical System

table.

So:

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

[ocatmetamath]

I came across this "bug" (am I going crazy on this or what!!!)

in the latest set.mm -- downloaded yesterday, 10/17:

mmj2 is able to pull up suctr and suctrALT and do ProofFormat = Normal and re-unify them.

That's what I would do. Save those .mmp's. Then write a shell script to find every other

case of variables or logical hypotheses inside the compressed proof paren list. And

modify metamath.exe to validate its input better (just add a double-check validation

that peeks at the paren list...run that validator on every new master candidate.)

And really, I believe in ProofFormat = Normal for set.mm backups of each new Master:

decompress set.mm and zip it up. Not too big, and save from bugs. 

On Sunday, October 14, 2018 at 9:36:44 PM UTC-7, ocatmetamath wrote:

[Norman Megill]

I'm a little bit confused, maybe I'm not looking closely enough.  What is the bug?

[ocatmetamath]

P.S. from my notes:

=============================================================

22) 10/18 discovered that suctr and suctrALT contain

        "illegal" compressed proofs: 

    suctr $p |- ( Tr A -> Tr suc A ) $=

      ( vz vy wtr cv wcel csuc wa wi wal wceq w3a sssucid id simpld trel sseldi

      adantl ex syl 3impib syl3an 3expia adantr eleqtrd wo simprd elsuci mpjaod

      idi alrimivv dftr2 biimpri ) ADZBEZCEZFZUPAGZFZHZUOURFZIZCJBJZURDZUNVBBCU

      NUTVAUNUTHUPAFZVAUPAKZUNUTVEVAUNUTVELAURUOAMZUNUNUTUQVEVEUOAFZUNNUTUQUSUT

      NZOZVENUNUQVELVHIUNUQVEVHAUOUPPUAUJUBQUCUTVFVAIUNUTVFVAUTVFHZAURUOVGVKUOU

      PAUTUQVFVJUDVFVFUTVFNRUEQSRUTVEVFUFZUNUTUSVLUTUQUSVIUGUPAUHTRUISUKVDVCBCU

      RULUMT $.

    suctrALT $p |- ( Tr A -> Tr suc A ) $=

      ( vz vy wtr cv wcel csuc wa wi wal wceq simpr vex elsuc sylib simpl eleq2

      wo syl6 mpdi syl5ibcom elelsuc trel exp3a adantrd syl8 jao alrimivv dftr2

      sylibr ) ADZBEZCEZFZUMAGZFZHZULUOFZIZCJBJUODUKUSBCUKUQUMAFZUMAKZRZURUQUPV

      BUNUPLUMACMNOUKUQVAURIZVBURIZUQVAULAFZURUQUNVAVEUNUPPUMAULQUAULAUBZSUKUQU

      TURIVCVDIUKUQUTVEURUKUNUTVEIUPUKUNUTVEAULUMUCUDUEVFUFUTURVAUGSTTUHBCUOUIU

      J $.

 

Although that is a production bug, and it might have

        been caused by a mmj2 bug that I just fixed, THAT

        is irrelevant because mmj2 v2.5.2.1017 PA GUI is able to 

decompress those proofs just fine ... and then it commits 

        its own crime and puts the bugs back [... Still shakin' it, Boss!]

        slightly differently (if you study the paren lists).

$=  ( vz vy wtr cv wcel csuc wa wal wceq w3a sssucid simpld trel sseldi adantl

    wi id ex syl 3impib syl3an 3expia adantr eleqtrd wo simprd elsuci alrimivv

    idi mpjaod dftr2 biimpri ) ADZBEZCEZFZUPAGZFZHZUOURFZQZCIBIZURDZUNVBBCUNUT

    VAUNUTHUPAFZVAUPAJZUNUTVEVAUNUTVEKAURUOALZUNUNUTUQVEVEUOAFZUNRUTUQUSUTRZMZ

    VERUNUQVEKVHQUNUQVEVHAUOUPNUAUJUBOUCUTVFVAQUNUTVFVAUTVFHZAURUOVGVKUOUPAUTU

    QVFVJUDVFVFUTVFRPUEOSPUTVEVFUFZUNUTUSVLUTUQUSVIUGUPAUHTPUKSUIVDVCBCURULUMT

    $.

$d y z 

$d A y 

$d A z 

=============================================================

[ocatmetamath]

Hi Norm, I did not see your query before I posted. 

The "bug" is that "vx" is inside the paren list. That's a variable!

Variables are supposed to be encoded in the proofs by 

references to VarHyp's, which are not explicitly included

in the paren list by convention. 

MandHyp converts to 1 -> m-1

LogHyp converts to m-> n-1

Assrt converts to n->infinity.

Only Assrt's in the paren list because the

other reference numbers are known implicitly

by the Theorem's Mandatory Hypothesis list/

array (and its order, which is fixed for use by

later theorems.)

Then those numbers are converted to base ?26?

And repeated subproofs are eliminated by

changing a later references to an RPN subtree

to an earlier identical RPN subtree. 

OK. Is that right.

[ocatmetamath]

P.S. One way to correct the files --> in v2.5.2.101?9? follows:

ProofAsstProofFolder,myproofs/TL/extract

TheoremLoaderMMTFolder,myproofs/TL/extract

SystemOutputFile,rptout/sysoutExport-001.txt,update,""

ProofAsstExportToFile,10,ProofAsstExport-001.txt,update,un-unified,NotRandomized,NoPrint,NoDeriveFormulas

SystemOutputFile,rptout/sysoutExport-001-MMT-IMPORT.txt,update,""

* java urps on next step w/stack out of space error when

* "*" is used instead of some 'n' in the ProofAsstExportToFile comamand

UnifyPlusStoreInLogSysAndMMTFolder,*,ProofAsstExport-001.txt,NoPrint

At the end of that process every theorem has its own .mmt

file in myproofs/TL/extract. ... 

Then once you figure out which proofs have errors one could, 

easily enough, pull the fixes manually, if there aren't too many.

[Norman Megill]

On Thursday, October 18, 2018 at 10:11:20 AM UTC-4, ocatmetamath wrote:

Hi Norm, I did not see your query before I posted. 

The "bug" is that "vx" is inside the paren list. That's a variable!

Variables are supposed to be encoded in the proofs by 

references to VarHyp's, which are not explicitly included

in the paren list by convention. 

I am still confused.  There is no "vx" in the paren list.  If you mean "vz", z is not a "mandatory" variable per the spec but is an "optional" variable used as a dummy variable in the proof, so it must be mentioned in the paren list.

Norm

[ocatmetamath]

<<I am still confused.  There is no "vx" in the paren list.  If you mean "vz", z is not a "mandatory" variable per the spec but is an "optional" variable used as a dummy variable in the proof, so it must be mentioned in the paren list. >>

Ha! You're right! Except 'vz' is a VarHyp -- of the "optional" variety as you pointed out.

So that's ok then. Super. Case closed :-)

[ocatmetamath]

OK, the big day has arrived for Theorem Loader. I just uploaded

v2.5.2.1018 to ocatmetamath-patch-2 at github. It contains

a new and improved TL batch command plus the Help 

documentation for the others. 

I am attaching a copy of today's RunParmsTest.txt which

uses TL and PA batch test commands to prove some things:

it runs a loops for one or all where a theorem is extracted,

updated back into the system and then re-extracted -- then

the .mmp's are compared, before and after update.

I ran this test on all theorems up to "mathbox", which is > 22000

theorems. All but 3 came out identical:

uzaddcl

faclbnd4lem4

ipasslem1

Notice that the first extract of .mmp's was nice enough to provide formulas

on the proof steps but not Ref labels. So to update a unification search

must be performed. At first glance proof subtrees changed order... I reran

the test with macro's and all of the mmj2-IQ-engine (transformations, autocomplete,

superautoderive....just kidding...everything

off except for Proof Compression. (And recall that the reason I am monkeying

with TL is because it never had proof compression fully installed.)

Any clues welcome. And I think you should now try v2.5.2.1018 because it is better

than ever. Really :-)

[David A. Wheeler]

On Thu, 18 Oct 2018 19:11:09 -0700 (PDT), ocatmetamath <b252...@gmail.com> wrote:
> OK, the big day has arrived for Theorem Loader. I just uploaded
> v2.5.2.1018 to ocatmetamath-patch-2 at github. It contains
> a new and improved TL batch command plus the Help
> documentation for the others.

Will you be distributing prebuilt files?

--- David A. Wheeler

[David A. Wheeler]

I'm not sure exactly where to report this...

The currently-recommended zip file for mmj2 per
<http://us.metamath.org/index.html#mmj2>
doesn't appear to run on Java 11 (OpenJDK 11 from https://jdk.java.net/11/)
on Windows.

I removed the no-longer-working -Xincgc and ran:
java -Xms128M -Xmx512M -jar mmj2.jar RunParms.txt Y "" c:\cygwin64\home\dwheeler\mmj2 ""

Result:
Exception in thread "main" java.lang.NumberFormatException: For input string: "."
at java.base/java.lang.NumberFormatException.forInputString(NumberFormatException.java:65)
at java.base/java.lang.Integer.parseInt(Integer.java:638)
at java.base/java.lang.Integer.parseInt(Integer.java:770)
at mmj.util.BatchMMJ2.checkVersion(BatchMMJ2.java:130)
at mmj.util.BatchMMJ2.<init>(BatchMMJ2.java:40)
at mmj.util.BatchMMJ2.main(BatchMMJ2.java:51)

Perhaps a more recent zip file works? Or I've made some other mistake? Thoughts?

--- David A. Wheeler

P.S. Contents of RunParms.txt is:

LoadFile,C:\cygwin64\home\dwheeler\set.mm\set.mm
VerifyProof,*
Parse,*
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
ProofAsstDeriveAutocomplete, yes
ProofAsstUseAutotransformations, yes,no,yes
RunProofAsstGUI
RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel
*done

[ocatmetamath]

We received a patch for that thing and I applied it. J. Kingdon

sent it to the mmj2 master with a pull:

See mmj.util.BatchMMJ2.java

/*
* Checks to see that the version of Java is
* sufficiently advanced to support mmj2.
* <p>
* (((Java 1.5 is the minimum as of May 2008 but
* this is subject to change if absolutely necessary.)))
* <p>
* @throws IllegalArgumentException if Java version is
* too ancient.
*/
public static void checkVersion() throws IllegalArgumentException {
final String javaVersion = System
.getProperty(UtilConstants.JAVA_VERSION_PROPERTY_NAME);


final String[] versionComponents = javaVersion.split("\\.");
final int maj = Integer.parseInt(versionComponents[0]);


final int min = Integer.parseInt(versionComponents[1]);


if (maj < UtilConstants.JAVA_VERSION_MMJ2_MAJ
|| maj == UtilConstants.JAVA_VERSION_MMJ2_MAJ
&& min < UtilConstants.JAVA_VERSION_MMJ2_MIN)
throw new IllegalArgumentException(
UtilConstants.JAVA_VERSION_MMJ2_RUNTIME_ERROR_MSG + javaVersion);

[ocatmetamath]

also, the macro language may have differences so 

it might be like a lobotomy for proof assistancy

[ocatmetamath]

Absolutely not. I uploaded mmj2.jar into the ocatmetamath-patch-2 branch -- which

is like 115 commits ahead of the mmj2 "master". And glauco has been using

my mmj2.jar -- very trusting person, haha. So I upload but do not distribute. 

I expect some people would recompile, which is almost easy enough for

a caveman to do it, or a monkey, if Eclipse is installed (am using June 2018,

Photon.) 

Here's my agenda. I've been fixing bugs for 5 weeks. 72 modules changed,

maybe 200 hours of work. Now, I've cleaned up Settings, Search (mostly),

and Theorem Loader, and fixed a few other things. I will now halt bug fixes

unless they're life changing problems and focus on auditing my work, testing

and making cleaning my rude chg comments out of the code so it matches

the existing style, which is very neat. I definitely plan to produce a few parallel

tests showing some amount of reliability, but given the amount of code

changes I will need actual users testing too. And that's my agenda. Right

now I think my branch is the apex, the lead branch and everyone should get

ready to use it. I cannot imagine y'all staying at the current level, so forward

is the only choice. No hurry, but I need to get these changed modules off

the operating table and back to work.

[ocatmetamath]

Here is a list of additions to mmj2 for testing use. I feel they

will be beneficial in the near and medium term. And quick

to code, except for the automated test file comparisons.

If you have any questions, wish more detail or propose other

ideas, please input.

- New RunParm commands (and call interfaces, of course):

- IncludeRunParmFile,xxxxxxx.txt (optional, user impact zero)

- PrintSettings

- PrintRunParmCommands,list|details(default)

- BatchVolTestGovernorLimit,999999999 (hardcoded at 10!)

    - New RunParm file dispositions: "append" and "void"

     (added to existing "new" and "update", esp useful for SysOut)

- 7th BatchMMJ2 arg: runparm override file name (provides string

 replacements to the user's RunParms file; optional, user impact zero)

- canonicalize RunParm and exec/cmd file name/path args for 

 macs vs win (/ vs \) to match the run platform

- automate comparisons (shell, runparm or python or java?)

 (I envision test reports and extract files being emitted into

                  an output repository holding the results of a group of tests;

 this helps humans look at the stuff -- but easily enough a program

                  could (should!?) scan pairs of directories and their sub-directories

 comparing all changes

                  and listing additions/deletions.)

- mmj2 (as a ) svc call interface widened -> or just pass batch framework!

[ocatmetamath]

Attached is my review of the changed modules based on file comparisons

between ocatmetamath-patch-2 and a fresh download of the mmj2

master at digama-mmj2, if memory serves. .csv and .xlsx. 

[ocatmetamath]

Here, I think a .pdf work better for casual viewing:

(attached)

[ocatmetamath]

I am now planning to work on building a test framework for mmj2.

the "patch 2" mmj2.jar file will be stable until someone reports a bug

in it :-)

I am envisioning using the proposed new RunParm commands in the prior

post to build this thing. With symbolic replacements of strings

in (test) RunParms, combined with an include-file capability,

it will be simple to build composable test kits based on RunParms.

And being able to write "append" or "void" to the output reports

will be helpful! I can see this now. It will be beautiful.

* * *

Here is an example of a .mm file that could be used in testing

    mmj2-mod-001/data/mm/UT3.mm

There are many more in the mmj2 directory, including .mmp and

RunParm files. A significant capital resource.

And, I think, with some small automation of test setup and

subsequent output file comparisons it will be fairly easy to

set up something where you say "run all feature tests"

and get back a report teling you if anything requires attention.

Anyone who wishes to participate in analysis/design/coding

let me know. I favor a language agnostic approach that

will enable someone to dump/replace/modify the test runner

code (with a wee bit of werk.)

This should be fun. One obvious goal is to make the test repository

accessible to everyone for contributions and use. How to make

everything stupid simple and failsafe-proofed  is the question. It

might not be simple enough for an ape to do (... I do not know. I

imagine it would depend on finding suitable motivations.)

[David A. Wheeler]

On October 21, 2018 7:58:36 PM EDT, ocatmetamath <b252...@gmail.com> wrote:
>I am now planning to work on building a test framework for mmj2.

Excellent. I think it is important in particular to test and ensure that things that should not verify are rejected.



--- David A.Wheeler

[ocatmetamath]

I am attaching my pre-first draft analysis of 'mmj2testbox'. 

The choice of writing in java would mean being able to run 

it from inside mmj2 -- or vice versa via the mmj2 Svc Feature.

Alternatively, writing in Python 3 means perhaps quicker

coding and the possibility of executing other commands

from within a 'mmj2testbox' run. Also, I intended it to be

outside of mmj2 for safety and sanity because during 

testing things sometimes get haphazard. 

If this works out as planned, it would mean being able

to download 'mmj2testbox', fill out a simple TestQuestionaire,

'tq', and then immediately setup and run verification tests

that the mmj2 installation is working in your new or changed

environment. So that would be good. Also, there will be

categories of tests, such as quick, volume, and feature

plus a normal, standard startup of the PA GUI. What I mean is,

there will/ought to be a standard suite of built-in tests

that come with 'mmj2testbox' requiring no adjustments

by the user. That is my intent.

I think this will take me a few weeks to work out. Any

feedback is welcome. 

[ocatmetamath]

OK, this is the Last Go Round for my 'mmj2tbox' specs. Until after coding :-)

The specs are attached. Not as good a read as this, Ken Kesey's best stuff:

    https://en.wikipedia.org/wiki/Last_Go_Round

[ocatmetamath]

I updated the attached 'test notes 1.txt' file in the previous post.

The 'spec' is getting real close to 'coding time', but I'll probably experiment

with fleshing out the directory structure with some real data and settings.

I think a motivated reader might appreciate my documentation. Everyone

else, no way. Not a fun read unless you're interested in running mmj2

in a vastly better way in the far future. Heh. (As far as I can tell, only

glauco has not yet written his own proof assistant!)

P.S. [fl] I saw Junyan Xu's post  this morning so I guess you'll be retracting

your jokes about my idea of using set.mm to teach AI's -- they

won't be RTFM after all! This is a perfect example of the motivation to

get Metamath into "the cloud" and to have a "common computing

environment" there. The cloud is where accelerator chips are for rent.

All kinds, AI, dataflow, FPGA (see Xilinx), etc. I remember well trying

to prove the first 100 set.mm theorems. What a chore. I bet google 

can do it in 2 minutes starting from zero. Maybe. Metamath is perfect

for teaching AI's because the files are self-defining. I'm interested in

new technology. That's where the $$$ is too.

On Thursday, October 25, 2018 at 12:50:14 PM UTC-7, ocatmetamath wrote:

I am attach a revised "analysis", which is morphing into a skeletal design.

And I am attaching a sample python3 program that calls mmj2 and waits

for it to finish. That is interesting. Glad it works.

So this "tester" project, "mmj2tbox", is shaping up as a wrapper around

mmj2 for pumping data through different versions of mmj2 in different

environments and capturing the output and then comparing it automatically.

It would be possible to do other things besides "testing", such as long-running

jobs to ... prove things?

The gist of this is having runparm include files and symbolic replacements

into a library of saved runparms files. Then tests are set up -- each runparm

file is considered a test. And the user's test variables, their 'tq.txt', are applied

to the runparms. One interesting thing is that a test can be stored in a

folder for a certain DB environment, such as set.mm, but then run in any

db environment. So your TQ variations are applied to a static library of

tests to create the current test Scenario. 

It'll be great. Once I get this going and run some parallel tests, I am 

interested in going through every "Feature" of mmj2 and trying to set

up a simple test that at least does something observable for the test.