LaTeX Warning: Reference `eq:ax-1' on page 1 undefined on input line

[Mike E]

I'm using set.mm version of 10-Dec-2017 and metamath binary, compiled from source at the end of 2017. I'm trying to compile latex code, generated by metamath command:

metamath 'read set.mm' 'open tex simples.latex' 'set width 250' 'show statement id1 /tex' 'show proof id1 /tex' 'close tex' 'exit'

when i type command "latex simples.latex" there are few errors dumped to terminal:

LaTeX Warning: Reference `eq:ax-1' on page 1 undefined on input line 39.

LaTeX Warning: Reference `eq:ax-2' on page 1 undefined on input line 39.

LaTeX Warning: Reference `eq:ax-mp' on page 1 undefined on input line 39.

and compiled dvi contains question marks "??" near the steps instead of links to the axioms. When i try to add metamath commands related to the axioms like 'show statement ax-1 /tex' before or after the commands related to the theorem id1 i see the same errors. The generated file contains the axioms definition labeled by "\label{axi:ax-1}" not by "\label{eq:ax-1}". How can I generate correct latex file with working links?

[Norman Megill]

Thank you for your report.

The LaTeX functionality has been poorly supported, mostly because hardly anyone uses it.  I've used it maybe 3-4 times in the past decade, to generate the starting LaTeX code for a formula for an article or a slide that I then customize by hand to conform to publication conventions.

I agree these problems are not acceptable, and I will look at them to see what I can do.  I'll post back here in a few days when I have some answers.

Norm

[Norman Megill]

I looked into this, and there doesn't seem to be a problem with the Metamath program.  Some issues related to this were fixed about a year ago, so your 10-Dec-2017 version should work.

First, you need to include all statements (axioms and previous theorems) that the proof references so that the proof will be able to hyperlink back to them.  If you want to include all proofs back to the beginning, you can get a (recursive) list of statements needed with "show trace_back id1/essential".  If you want to include just the id1 proof along with the statements (without proofs) the id1 proof references, it's a little more awkward: "./metamath 'r set.mm' 'sh p id1/statem' q | egrep '\$a|\$p'".  (In the case of id1, only previous axioms are referenced, so these 2 lists will have the same statements.)

Second, you need to run latex twice.  The first run generates a new .aux file but gives warnings if the .aux file is missing or an old version.  The second run reads the new .aux file and produces no warnings.  This is a characteristic of LaTeX not related to Metamath.

Here is the output of a sample run, where I used pdflatex to generate a pdf file directly:

$ ./metamath 'r set.mm' 'o t a.tex' 'set w 250' 'sh st ax-1,ax-2,ax-mp,id1/tex' 'sh p id1/tex' q
Metamath - Version 0.161 2-Feb-2018           Type HELP for help, EXIT to exit.
MM> r set.mm
...
MM> q
The LaTeX file "a.tex" was closed.

$ pdflatex a.tex
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/W32TeX) (preloaded
...
LaTeX Warning: Reference `eq:ax-1' on page 1 undefined on input line 79.
LaTeX Warning: Reference `eq:ax-1' on page 1 undefined on input line 79.
LaTeX Warning: Reference `eq:ax-2' on page 1 undefined on input line 79.
...

$ pdflatex a.tex
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/W32TeX) (preloaded
...
[no warnings]
...

$ ls -l a.pdf
-rwxrwx---+ 1 norm norm 86127 Apr 25 07:14 a.pdf

Some additional remarks:

1. As for "\label{axi:ax-1}" vs. "\label{eq:ax-1}", the first labels the the axiom/theorem description, and the second labels the formula of the axiom/theorem.  The "\ref{...}" in the proof links back to the formula and not the description, since I thought that was more useful for the purpose of following a proof.  If you prefer to have it link to the description, you can do a global edit to the \ref's.

2. The formatting of the LaTeX output for things like long formulas may not always be ideal, and some manual adjustment may be needed to produce professional-looking documents.  There aren't any plans right now to do major enhancements with things like intelligent line breaks in the output formulas.  If minor formatting issues are found that could be fixed with small program tweaks, I'm usually happy to consider those.

3. If your goal is to produce a document for self-study that can be viewed off-line, the pdf file will be enormous for more than a few theorems at the beginning of set.mm.  The web pages may be easier to navigate and can be downloaded for off-line viewing as mpeuni.tar.bz2 (70MB, unpacks to 1.6GB) on the Metamath Home Page.

Norm

On Tuesday, April 24, 2018 at 10:27:59 AM UTC-4, Mike E wrote:

[Mike E]

Thank you very much, Norman. I will test it as soon as possible.

вторник, 24 апреля 2018 г., 17:27:59 UTC+3 пользователь Mike E написал: