Multiple Typesetting Comments

[Brian Larson]

I'm trying to generate LaTeX of my definitions and theorems.  My .mm file reads set.mm.

I tried to put my latexdef statements in a $t comment in my .mm file, but got complaints.

So I have been appending my latexdef statements to the end of the $t comment in set.mm--something I'd rather not do.

I've successfully generated .tex output which I have copied into my document.  However, now I get an error message I do not understand:

MM> open tex df.tex

Created LaTeX output file "df.tex".

Reading definitions from $t statement of bless-p.mm...

?Error: There is no $t command in the file "bless-p.mm".

The file should have exactly one comment of the form $(...$t...$) with

the LaTeX and HTML definitions between $t and $).

?There was an error in the $t comment's LaTeX/HTML definitions.

MM> 

Of course, there is no $t comment in my .mm file, and I didn't get such an error previously.

Q1)  Are there plans to allow one $t comment per .mm file (even if they import other .mm files)?

Q2)  Are there suggestions what error my recent work introduced to cause LaTeX generation to fail?

--Brian

[Norman Megill]

You are right that only one $t comment is allowed per database.

The main reason we don't allow multiple $t comments is that it is convenient for maintenance to have everything in one place. "write source set.mm /split" will create it as a file called set-typeset.mm that can be edited independently from the rest of set.mm. If multiple $t's are scattered around in many different places, we would lose that modularity. Once we go down the path of allowing multiple $t's, we can't (easily) go back.

We can open up a discussion about the advantages and disadvantages of multiple $t's. But even if we decide to go with it, it would take some time to code, so it won't solve your immediate problem. For now, you will have to edit set.mm (or set-typeset.mm) to add the latexdefs that you need.

As for your error message, if you have "$[ set.mm $]" in your bless-p.mm file, I was unable to reproduce it. Perhaps you can provide a simple test case that reproduces the problem.  You can also run the metamath.exe command "verify markup * /f" which (among other things) will do an error check on the $t comment.

Norm

[Brian Larson]

Norm,

Thanks for your response.

I found the problem, and I thought I'd added a note to my initial issue.

Somehow I had inadvertently deleted the $t from set.mm. 

I suspect that I'd searched for $t and then bumped return or spacebar.

I wondered what those special comments were; now I know.

I much appreciate your creation of Metamath, with which i am formalizing a temporal logic to specify timing behavior of embedded systems.

Thank you, again.

--Brian

.

--
You received this message because you are subscribed to a topic in the Google Groups "Metamath" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/metamath/3NDUZ4AVEl8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/68eb4f91-e50c-4091-9857-54360f225c71n%40googlegroups.com.

[David A. Wheeler]

On Sep 20, 2021, at 11:55 AM, Brian Larson <brianral...@gmail.com> wrote:

My mistake:  When editing set.mm, I inadvertently deleted the $t

I would still request that one $t comment be allowed per file, so my errors would be confined to my .mm files rather than added latexdef commands to set.mm.

Norm will ultimately decide if more than one $t is allowed.

That said, once “more than one $t” is allowed, I recommend adding no more restrictions.

if “more than 1” $t is allowed, just allow them.

--- David A. Wheeler