Thanks for the bug report.
The error is due to this:
! pdfTeX error (font expansion): auto expansion is only possible with scalable
fonts.
\AtBegShi@Output ...ipout \box \AtBeginShipoutBox
\fi \fi
I will try to look into what is going on at this point in the file to see if
there is something obviously wrong in our LaTeX sources. This error doesn't
manifest on my setup, but that's not necessarily an excuse :)
See also
https://tex.stackexchange.com/questions/10706/pdftex-error-font-expansion-auto-expansion-is-only-possible-with-scalable
for some discussion.
Michael
On 30/7/18, 03:42, "Mario Xerxes Castelán Castro" <[email protected]>
wrote:
Hello. On HOL4 commit “37bf2ea80” I run "make description" within the
directory "Manual" and get the following error:
$ make description
(cd Description; Holmake; cd ..)
Working in $(HOLDIR)/examples/misc
Working in $(HOLDIR)/tools/cmp
Working in $(HOLDIR)/Manual/Tools
Working in $(HOLDIR)/Manual/Description
description.pdf
FAILED! <C>
Reference `sec:simpLib' on page 85 undefined on input line 590
Reference `sec:traces' on page 146 undefined on input line 3602
Latexmk: Summary of warnings:
Latex failed to resolve 18 reference(s)
Latex failed to resolve 17 citation(s)
Collected error summary (may duplicate other messages):
pdflatex: Command for 'pdflatex' gave return code 256
Latexmk: Use the -f option to force complete processing,
unless error was exceeding maximum runs of latex/pdflatex.
Latexmk: Errors, so I did not complete making targets
====> DESCRIPTION made
I am using Debian 9 and I am attaching the file for “description.pdf”
generated in “.hollogs”. Please tell me how to solve this problem to
build the description manual.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
