PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
170 stars 28 forks source link

lakeblueprint pdf not working on fresh blueprint #24

Closed mdgeorge4153 closed 5 months ago

mdgeorge4153 commented 5 months ago

It seems like the leanblueprint macros are not defined for some reason in my environment.

I created a brand new repo and lean blueprint:

lake new blueprint-mwe
cd blueprint-mwe
git ci -am "initial commit"
leanblueprint new

I then edited blueprint/src/content.tex as follows:

\newtheorem{theorem}{Theorem}

\begin{theorem}
    \label{thm:example}
    \notready
    Exampl
\end{theorem}

When I run leanblueprint pdf I get the following (some output elided):

Rc files read:
  /etc/LatexMk
  latexmkrc
Latexmk: This is Latexmk, John Collins, 20 November 2021, version: 4.76.
Latexmk: applying rule 'pdflatex'...
Rule 'pdflatex': File changes, etc:
   Changed files, or newly in use since previous run(s):
      '/home/mdgeorge/lean/blueprint-mwe/blueprint/print/print.aux'
------------
Run number 1 of rule 'pdflatex'
------------
------------
Running 'xelatex -synctex=1  -recorder -output-directory="/home/mdgeorge/lean/blueprint-mwe/blueprint/print"  "print.tex"'
------------
This is XeTeX, Version 3.141592653-2.6-0.999993 (TeX Live 2022/dev/Debian) (preloaded format=xelatex)
 restricted \write18 enabled.
entering extended mode
(./print.tex
LaTeX2e <2021-11-15> patch level 1
L3 programming layer <2022-01-21>
(/usr/share/texlive/texmf-dist/tex/latex/base/report.cls

...

(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty))
(/home/mdgeorge/lean/blueprint-mwe/blueprint/print/print.out)
(/home/mdgeorge/lean/blueprint-mwe/blueprint/print/print.out)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) [1] (./content.tex
! Undefined control sequence.
l.13     \notready
PatrickMassot commented 5 months ago

I am sorry, this macro was forgotten in the template. You can add it to your macros/print.tex file as in a8395d2c9cb82516b0.