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.
Latexmk: This is Latexmk, John Collins, 1 January 2015, version: 4.41.
Rule 'pdflatex': File changes, etc:
Non-existent destination files:
'description.pdf'
------------
Run number 1 of rule 'pdflatex'
------------
------------
Running 'pdflatex -recorder "description.tex"'
------------
Latexmk: applying rule 'pdflatex'...
This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016/Debian)
(preloaded format=pdflatex)
restricted \write18 enabled.
entering extended mode
(./description.tex
LaTeX2e <2017/01/01> patch level 3
Babel <3.9r> and hyphenation patterns for 3 language(s) loaded.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/fleqn.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk12.clo))
(/usr/share/texlive/texmf-dist/tex/latex/tocbibind/tocbibind.sty
Package tocbibind Note: Using chapter style headings, unless overridden.
) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/makeidx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/alltt.sty) (../LaTeX/layout.sty
(/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ifpdf.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ifvtex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty))
(/usr/share/texlive/texmf-dist/tex/latex/stix/stix.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def)))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/t1bch.fd)
(/usr/share/texlive/texmf-dist/tex/latex/base/t1cmtt.fd))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(../LaTeX/proof.sty
LaTeX Warning: You have requested package `../LaTeX/proof',
but the package provides `proof'.
) (/usr/share/texlive/texmf-dist/tex/latex/supertabular/supertabular.sty)
(../../src/TeX/holtexbasic.sty
(/usr/share/texlive/texmf-dist/tex/latex/underscore/underscore.sty)
(/usr/share/texlive/texmf-dist/tex/latex/fancyvrb/fancyvrb.sty
Style option: `fancyvrb' v2.7a, with DG/SPQR fixes, and firstline=lastline fix
<2008/02/07> (tvz))) (../LaTeX/commands.tex)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
Package hyperref Message: Driver (autodetected): hpdftex.
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/breakurl/breakurl.sty
(/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkeyval.tex
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkvutils.tex)))
Package breakurl Warning: You are using breakurl while processing via pdflatex.
(breakurl) \burl will be just a synonym of \url.
(breakurl) on input line 48.
) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/centernot.sty)
Writing index file description.idx
(./description.aux (./title.aux) (./preface.aux) (./system.aux) (./drules.aux)
(./conv.aux) (./tactics.aux) (./theories.aux) (./definitions.aux))
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls1stix.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls2stix.fd)
*geometry* driver: auto-detecting
*geometry* detected driver: pdftex
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-bch.cfg)
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/grfext.sty)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./description.out) (./description.out) (./title.tex
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/t1ptm.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-ptm.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls1stixscr.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls2stixex.fd)
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls1stixfrak.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls1stixbb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls2stixcal.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls1stixsf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stix/ls2stixtt.fd)
<../Logo/lantern.pdf, id=538, 403.5075pt x 436.63126pt>
<use ../Logo/lantern.pdf> [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}
<../Logo/lantern.pdf>] [2]) (./preface.tex
LaTeX Warning: Citation `Church' on page 3 undefined on input line 30.
LaTeX Warning: Citation `Hanna-Daeche' on page 3 undefined on input line 33.
LaTeX Warning: Citation `Edinburgh-LCF' on page 3 undefined on input line 44.
[3]
LaTeX Warning: Citation `sml' on page 4 undefined on input line 69.
) [4] (../LaTeX/ack.tex [5]
LaTeX Font Warning: Font shape `U/lasy/m/n' in size <7.5> not available
(Font) size <7> substituted on input line 74.
[6]) [7] [8] (./description.toc) [9] (./system.tex [10]
Chapter 1.
LaTeX Warning: Reference `sec:bossLib' on page 11 undefined on input line 13.
[11] [12] [13] [14]
LaTeX Warning: Reference `sec:quotation-antiquotation' on page 15 undefined on
input line 433.
[15] (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1bch.fd) [16]
LaTeX Warning: Reference `sec:parsing-printing' on page 17 undefined on input l
ine 549.
[17]
Overfull \hbox (71.72604pt too wide) in paragraph at lines 598--598
[]\T1/cmtt/m/n/10.95 unification failure message: Attempt to unify different ty
pe operators: num$num and min$bool[]
Overfull \hbox (1636.26561pt too wide) in paragraph at lines 601--601
[] \T1/cmtt/m/n/10.95 "on line 1, characters 9-13:\n\nType inference failure:
unable to infer a type for the application of\n\n$= (x :num)\n\non line 1, cha
racters 4-14\n\nwhich has type\n\n:num -> bool\n\nto\n\n(x :num) = (1 :num)\n\n
on line 1, characters 9-13\n\nwhich has type\n\n:bool\n\nunification failure me
ssage: Attempt to unify different type operators: num$num and min$bool\n",[]
[18] [19] [20] [21]
LaTeX Font Warning: Command \small invalid in math mode on input line 847.
[22] [23] [24] [25] [26] [27] [28] [29] [30] [31]
LaTeX Warning: Reference `Holmake' on page 32 undefined on input line 1825.
[32] [33] [34] [35] [36] [37]) [38] (./drules.tex
Chapter 2.
[39] [40] [41] [42] [43] [44] [45] [46]
(/usr/share/texlive/texmf-dist/tex/latex/base/t1cmss.fd) [47] [48] [49]
[50] [51] [52] [53] [54] [55] [56]) [57] (./conv.tex [58]
Chapter 3.
LaTeX Warning: Citation `lcp-rewrite' on page 59 undefined on input line 62.
LaTeX Warning: Citation `new-LCF-man' on page 59 undefined on input line 62.
[59]
Underfull \vbox (badness 10000) has occurred while \output is active [60]
[61] [62] [63] [64] [65] [66] [67] [68] [69] [70] [71] [72] [73] [74]) [75]
(./tactics.tex [76]
Chapter 4.
Underfull \vbox (badness 2875) has occurred while \output is active [77]
[78]
LaTeX Warning: Reference `sec:goalstack' on page 79 undefined on input line 127
.
[79]
LaTeX Warning: Reference `sec:simpLib' on page 80 undefined on input line 227.
[80] [81] [82]
LaTeX Warning: Reference `sec:goalstack' on page 83 undefined on input line 395
.
[83] [84]
LaTeX Warning: Reference `sec:simpLib' on page 85 undefined on input line 590.
[85]
LaTeX Warning: Citation `new-LCF-man' on page 86 undefined on input line 640.
[86] [87] [88] [89]
LaTeX Warning: Citation `lcp-rewrite' on page 90 undefined on input line 1003.
LaTeX Warning: Citation `new-LCF-man' on page 90 undefined on input line 1003.
Underfull \vbox (badness 10000) has occurred while \output is active [90]
[91] [92]
Underfull \vbox (badness 10000) has occurred while \output is active [93]
Underfull \vbox (badness 10000) has occurred while \output is active [94]
Underfull \vbox (badness 10000) has occurred while \output is active [95]
[96] [97] [98]
Overfull \hbox (0.8116pt too wide) in paragraph at lines 1544--1554
\T1/bch/m/n/12 (-20) Where [] ab-bre-vi-ates []. []
[99]) [100] (./theories.tex
Chapter 5.
LaTeX Warning: Citation `Church' on page 101 undefined on input line 74.
LaTeX Warning: Citation `Leisenring' on page 101 undefined on input line 76.
LaTeX Warning: Citation `Andrews' on page 101 undefined on input line 77.
[101]
LaTeX Warning: Citation `Church' on page 102 undefined on input line 122.
[102] [103] [104] [105] [106]
LaTeX Warning: Reference `hidden' on page 107 undefined on input line 717.
[107] [108] [109] [110]
LaTeX Warning: Citation `Melham-banff' on page 111 undefined on input line 1125
.
[111] [112] [113] [114] [115] [116]
LaTeX Warning: Reference `sec:high-level-proof-steps' on page 117 undefined on
input line 1545.
[117] [118] [119] [120] [121] [122] [123]
LaTeX Warning: Citation `jrh:thesis' on page 124 undefined on input line 2045.
[124]
LaTeX Warning: Citation `hurd-thesis' on page 125 undefined on input line 2107.
[125] [126] [127] [128] <figs/lsl.pdf, id=1658, 216.81pt x 71.26625pt>
<use figs/lsl.pdf> <figs/lsr.pdf, id=1659, 227.85126pt x 71.26625pt>
<use figs/lsr.pdf> <figs/asr.pdf, id=1660, 225.84375pt x 71.26625pt>
<use figs/asr.pdf> <figs/ror.pdf, id=1661, 244.915pt x 71.26625pt>
<use figs/ror.pdf> <figs/rrx.pdf, id=1662, 271.0125pt x 89.33376pt>
<use figs/rrx.pdf> [129] [130 <./figs/lsl.pdf> <./figs/lsr.pdf> <./figs/asr.pdf
> <./figs/ror.pdf> <./figs/rrx.pdf>]
Overfull \hbox (30.79633pt too wide) in paragraph at lines 2445--2486
[]
[131] [132] [133]
Overfull \hbox (25.48067pt too wide) in paragraph at lines 2660--2660
[]\T1/cmtt/m/n/10.95 val it = $ [] $ ($\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/
10.95 x. MEM x [] $[]$ F) $\LS1/stix/m/n/10.95 á$ $Å$\T1/cmtt/m/n/10.95 x h t.
MEM x (h::t) $[]$ (x = h) $\LS1/stix/m/n/10.95 â$ \T1/cmtt/m/n/10.95 MEM x t: t
hm[]
[134] [135] [136] [137] [138]
Overfull \hbox (16.96732pt too wide) in paragraph at lines 3073--3083
\T1/bch/m/n/12 (-20) The higher-order [] func-tion[] []ex-em-pli-fies an-other
set of con-stants within the []
[139] [140] [141] [142]
Overfull \hbox (16.18005pt too wide) in paragraph at lines 3378--3378
[] \T1/cmtt/m/n/10.95 okpath R p $\LS1/stix/m/n/10.95 á$ \T1/cmtt/
m/n/10.95 finite p $\LS1/stix/m/n/10.95 á$ \T1/cmtt/m/n/10.95 R x r (first p) $
\LS1/stix/m/n/10.95 á$ \T1/cmtt/m/n/10.95 P p $\LS1/stixsf/m/n/10.95 Ù$ \T1/cmt
t/m/n/10.95 P (pcons x r p)) $\LS1/stixsf/m/n/10.95 Ù$[]
[143]
LaTeX Warning: Reference `sec:quotation-antiquotation' on page 144 undefined on
input line 3491.
[144] [145]
LaTeX Warning: Reference `sec:traces' on page 146 undefined on input line 3602.
LaTeX Warning: Reference `sec:parseprint:fixities' on page 146 undefined on inp
ut line 3605.
LaTeX Warning: Reference `sec:parser:syntactic-patterns' on page 146 undefined
on input line 3605.
[146] [147] [148] [149] [150] [151] [152] [153] [154] [155] [156] [157]
[158]
LaTeX Warning: Reference `TFL' on page 159 undefined on input line 4548.
[159]
Overfull \hbox (0.8481pt too wide) in paragraph at lines 4642--4642
[] $ [] $ $\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/10.95 f g. (f = g) $[]$
(FDOM f = FDOM g) $\LS1/stix/m/n/10.95 á$ $Å$\T1/cmtt/m/n/10.95 x. x $\LS1/stix
/m/n/10.95 Ë$ \T1/cmtt/m/n/10.95 FDOM f $\LS1/stixsf/m/n/10.95 Ù$ \T1/cmtt/m/n/
10.95 (f ' x = g ' x)[]
Overfull \hbox (5.54622pt too wide) in paragraph at lines 4644--4644
[] $ [] $ $\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/10.95 P. P FEMPTY $\LS1/
stix/m/n/10.95 á$ \T1/cmtt/m/n/10.95 ($\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/10.95
f. P f $\LS1/stixsf/m/n/10.95 Ù$ $\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/10.95 x y
. x $\LS1/stix/m/n/10.95 Ì$ \T1/cmtt/m/n/10.95 FDOM f $\LS1/stixsf/m/n/10.95 Ù$
\T1/cmtt/m/n/10.95 P (f |+ (x,y))) $\LS1/stixsf/m/n/10.95 Ù$ $\LS1/stix/m/n/10
.95 Å$\T1/cmtt/m/n/10.95 f. P f[]
Overfull \hbox (5.66797pt too wide) in paragraph at lines 4649--4649
[] \T1/cmtt/m/n/10.95 FCARD (fm |+ (a,b)) = if a $\LS1/stix/m/n/10.9
5 Ë$ \T1/cmtt/m/n/10.95 FDOM fm then FCARD fm else 1 + FCARD fm[]
[160]
Overfull \hbox (6.98929pt too wide) in paragraph at lines 4689--4689
[] $\LS1/stix/m/n/10.95 Å$\T1/cmtt/m/n/10.95 x. DRESTRICT f r ' x =
if x $\LS1/stix/m/n/10.95 Ë$ \T1/cmtt/m/n/10.95 FDOM f $\LS1/stix/m/n/10.95 ã$
\T1/cmtt/m/n/10.95 r then f ' x else FEMPTY ' x[]
[161] [162] [163] [164] [165] [166] [167]) [168] [169] (./definitions.tex
[170]
Chapter 6.
LaTeX Warning: Reference `sec:bossLib' on page 171 undefined on input line 65.
[171] [172] [173] [174]
LaTeX Warning: Reference `CaseExp' on page 175 undefined on input line 340.
[175] [176] [177
! pdfTeX error (font expansion): auto expansion is only possible with scalable
fonts.
\AtBegShi@Output ...ipout \box \AtBeginShipoutBox
\fi \fi
l.476 \begin{hol}
! ==> Fatal error occurred, no output PDF file produced!
Transcript written on description.log.
Latexmk: Index file 'description.idx' was written
Latexmk: List of undefined refs and citations:
Citation `Andrews' on page 101 undefined on input line 77
Citation `Church' on page 101 undefined on input line 74
Citation `Church' on page 102 undefined on input line 122
Citation `Church' on page 3 undefined on input line 30
Citation `Edinburgh-LCF' on page 3 undefined on input line 44
Citation `Hanna-Daeche' on page 3 undefined on input line 33
Citation `Leisenring' on page 101 undefined on input line 76
Citation `Melham-banff' on page 111 undefined on input line 1125
Citation `hurd-thesis' on page 125 undefined on input line 2107
Citation `jrh:thesis' on page 124 undefined on input line 2045
Citation `lcp-rewrite' on page 59 undefined on input line 62
Citation `lcp-rewrite' on page 90 undefined on input line 1003
Citation `new-LCF-man' on page 59 undefined on input line 62
Citation `new-LCF-man' on page 86 undefined on input line 640
Citation `new-LCF-man' on page 90 undefined on input line 1003
Citation `sml' on page 4 undefined on input line 69
Reference `CaseExp' on page 175 undefined on input line 340
Reference `Holmake' on page 32 undefined on input line 1825
Reference `TFL' on page 159 undefined on input line 4548
Reference `hidden' on page 107 undefined on input line 717
Reference `sec:bossLib' on page 11 undefined on input line 13
Reference `sec:bossLib' on page 171 undefined on input line 65
Reference `sec:goalstack' on page 79 undefined on input line 127
Reference `sec:goalstack' on page 83 undefined on input line 395
Reference `sec:high-level-proof-steps' on page 117 undefined on input line
1545
Reference `sec:parseprint:fixities' on page 146 undefined on input line 3605
Reference `sec:parser:syntactic-patterns' on page 146 undefined on input line
3605
Reference `sec:parsing-printing' on page 17 undefined on input line 549
Reference `sec:quotation-antiquotation' on page 144 undefined on input line
3491
Reference `sec:quotation-antiquotation' on page 15 undefined on input line 433
Reference `sec:simpLib' on page 80 undefined on input line 227
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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
