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 . > On Sep 20, 2021, at 7:17 PM, Norman Megill <[email protected]> wrote: > > 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 > > On Sunday, September 19, 2021 at 10:35:46 PM UTC-4 [email protected] > wrote: > I'm trying to generate LaTeX of my definitions and theorems. My .mm file > reads set.mm <http://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 <http://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 > > > > > -- > 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 > <https://groups.google.com/d/topic/metamath/3NDUZ4AVEl8/unsubscribe>. > To unsubscribe from this group and all its topics, send an email to > [email protected] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/68eb4f91-e50c-4091-9857-54360f225c71n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/68eb4f91-e50c-4091-9857-54360f225c71n%40googlegroups.com?utm_medium=email&utm_source=footer>. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/C4253296-61D6-404F-BCC2-40B966F9C04C%40gmail.com.
