Attachment 1465764 Details for Bug 1605528 – build.log

build.log

build.log (text/plain), 32.00 KB, created by Mohan Boddu on 2018-07-20 15:51:39 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Mohan Boddu

Created: 2018-07-20 15:51:39 UTC

Size: 32.00 KB

patch

obsolete

>Encoding):
>(hyperref)                removing `\largett' on input line 3122.
>[58]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3147.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3147.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3157.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3157.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3170.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3170.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3185.
>[59] [60]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3256.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3266.
>Overfull \hbox (6.88857pt too wide) in paragraph at lines 3271--3279
>[]\OT1/cmr/m/n/12 Two names such as $[]$ and $[]$
>[61]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3331.
>[62]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3414.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3414.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3423.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3423.
>[63]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3442.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3442.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3453.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3453.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3463.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3463.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3476.
>[64] [65]
>Overfull \hbox (4.465pt too wide) in paragraph at lines 3551--3553
>[]\OT1/cmr/m/n/12 : Adds the for-mula 
>Overfull \hbox (0.8467pt too wide) in paragraph at lines 3565--3569
>[]\OT1/cmr/m/n/12 One of the ex-pres-sions in
>[66]
>Overfull \hbox (2.44466pt too wide) in paragraph at lines 3588--3593
>[]\OT1/cmr/m/n/12 The de-fined rules \OT1/cmtt/m/n/12 rewrite[] \OT1/cmr/m/n/12
> and \OT1/cmtt/m/n/12 rewrite-lemma[] \OT1/cmr/m/n/12 em-ploy the \OT1/cmtt/m/n
>/12 lemma[] \OT1/cmr/m/n/12 and \OT1/cmtt/m/n/12 replace[]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3599.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3599.
>[67]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3664.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3664.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3702.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3702.
>[68]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3724.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3724.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3761.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3761.
>[69]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3794.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3794.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3806.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3806.
>Overfull \hbox (1.63995pt too wide) in paragraph at lines 3821--3826
>[]\OT1/cmr/m/n/12 If the \OT1/cmr/m/it/12 hide? \OT1/cmr/m/n/12 flag is set to 
>\OT1/cmtt/m/n/12 t\OT1/cmr/m/n/12 , the equal-ity for-mula to which the apply-e
>xtensionality
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3828.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3828.
>[70]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3845.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3845.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3880.
>Overfull \hbox (0.10735pt too wide) in paragraph at lines 3890--3892
>[]\OT1/cmr/m/n/12 : Yields a sub-goal got by adding
>[71]
>Overfull \hbox (2.41719pt too wide) in paragraph at lines 3907--3909
>[]\OT1/cmr/m/n/12 : Adds an an-tecedent for-mula
>Overfull \hbox (8.62463pt too wide) in paragraph at lines 3938--3940
>[]\OT1/cmr/m/n/12 This means that
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3952.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3952.
>[72]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 3967.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 3967.
>Underfull \hbox (badness 10000) in paragraph at lines 4010--4011
>[73]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4011.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4011.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4073.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4073.
>[74]
>Overfull \hbox (8.33815pt too wide) in paragraph at lines 4079--4086
>[]\OT1/cmr/m/n/12 This com-mand has been su-per-seded by the more gen-eral \OT1
>/cmtt/m/n/12 induct-and-simplify[]
>Overfull \hbox (12.01611pt too wide) in paragraph at lines 4088--4093
>[]\OT1/cmr/m/n/12 : In-tro-duces an in-stance
>Overfull \hbox (1.02106pt too wide) in paragraph at lines 4094--4096
>[]\OT1/cmr/m/n/12 : Same as
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4100.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4100.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4116.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4116.
>[75]
>Overfull \hbox (12.57176pt too wide) in paragraph at lines 4142--4149
>[]\OT1/cmtt/m/n/12 (induct-and-simplify "i" :defs ! :theories "real[]props" :re
>writes
>Overfull \hbox (1.5012pt too wide) in paragraph at lines 4150--4156
>[]\OT1/cmr/m/n/12 : In-ducts ac-cord-
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4160.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4160.
>[76]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4209.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4209.
>Overfull \hbox (5.21255pt too wide) in paragraph at lines 4249--4255
>[]\OT1/cmr/m/n/12 : Ap-plies the
>[77]
>Overfull \hbox (3.93015pt too wide) in paragraph at lines 4256--4262
>[]\OT1/cmr/m/n/12 : Ap-plies mea-sure in-
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4266.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4266.
>Overfull \hbox (6.31776pt too wide) in paragraph at lines 4278--4293
>[]\OT1/cmr/m/n/12 Invokes the ap-pro-pri-ate in-stance of mea-sure in-duc-tion 
>us-ing \OT1/cmtt/m/n/12 measure-induct+[]\OT1/cmr/m/n/12 ,
>[78]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4317.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4317.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4331.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4331.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4359.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4359.
>[79]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4380.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4380.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4400.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4400.
>Overfull \hbox (1.74098pt too wide) in paragraph at lines 4411--4413
>[]\OT1/cmtt/m/n/12 (simple-measure-induct "i+j" ("i" "j"))\OT1/cmr/m/n/12 : In-
>serts mea-sure in-duc-tion on
>[80]
>Underfull \hbox (badness 2762) in paragraph at lines 4477--4477
>[]|\OT1/cmr/m/n/12 install rewrites, sim-plify, and stop
>Overfull \hbox (17.62482pt too wide) in paragraph at lines 4477--4478
>[][] 
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4479.
>[81]
>Overfull \hbox (5.77737pt too wide) in paragraph at lines 4491--4506
>[]\OT1/cmr/m/n/12 The \OT1/cmtt/m/n/12 assert[] \OT1/cmr/m/n/12 rule is a com-b
>i-na-tion of \OT1/cmtt/m/n/12 record[]\OT1/cmr/m/n/12 , \OT1/cmtt/m/n/12 simpli
>fy[]\OT1/cmr/m/n/12 , \OT1/cmtt/m/n/12 beta[]\OT1/cmr/m/n/12 , and \OT1/cmtt/m/
>n/12 do-rewrite[]\OT1/cmr/m/n/12 .
>[82] [83]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4639.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4639.
>[84]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4683.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4683.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4699.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4712.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4712.
>[85]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4745.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4745.
>Overfull \hbox (0.15298pt too wide) in paragraph at lines 4770--4772
>[]\OT1/cmr/m/n/12 The \OT1/cmr/m/it/12 defs\OT1/cmr/m/n/12 , \OT1/cmr/m/it/12 t
>he-o-ries\OT1/cmr/m/n/12 , \OT1/cmr/m/it/12 rewrites\OT1/cmr/m/n/12 , and \OT1/
>cmr/m/it/12 ex-clude \OT1/cmr/m/n/12 ar-gu-ments are as in \OT1/cmtt/m/n/12 ins
>tall-rewrites[]\OT1/cmr/m/n/12 . 
>[86]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4798.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4798.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4814.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4814.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4826.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4826.
>[87]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4850.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4850.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4863.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4863.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4894.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4894.
>[88]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4933.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 4933.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 4948.
>Overfull \hbox (8.52112pt too wide) in paragraph at lines 4960--4969
>[]\OT1/cmtt/m/n/12 simplify[] \OT1/cmr/m/n/12 is a prim-i-tive com-mand used in
> the def-i-ni-tion of \OT1/cmtt/m/n/12 assert[]\OT1/cmr/m/n/12 , \OT1/cmtt/m/n/
>12 do-rewrite[]\OT1/cmr/m/n/12 ,
>[89] [90]
>Overfull \hbox (0.36841pt too wide) in alignment at lines 5063--5069
> [][][] []
>[91] [92]
>Overfull \hbox (7.5846pt too wide) in paragraph at lines 5171--5176
>[]\OT1/cmr/m/n/12 : Flushes the de-ci-sion pro-ce-dure database
>[93]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5200.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5200.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5215.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5215.
>[94]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5266.
>[95] [96]
>Overfull \hbox (8.09053pt too wide) in paragraph at lines 5403--5406
>[]\OT1/cmr/m/n/12 Since
>Overfull \hbox (18.8172pt too wide) in paragraph at lines 5408--5409
>[]
>[97]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5427.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5427.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5438.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5438.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5448.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5448.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5470.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5470.
>[98]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5486.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5486.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5500.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5500.
>Overfull \hbox (18.74677pt too wide) in paragraph at lines 5523--5526
>[]\OT1/cmtt/m/n/12 (auto-rewrite-theory "sets[nat]" "sets[rational]" "list[]adt
>[nat]")
>[99]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5548.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5548.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5570.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5570.
>[100]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5609.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5626.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5626.
>Overfull \hbox (14.12337pt too wide) in paragraph at lines 5640--5643
>[]\OT1/cmtt/m/n/12 (stop-rewrite-theory "sets[nat]" "sets[rational]" "list[]adt
>[nat]")
>Overfull \hbox (8.99844pt too wide) in paragraph at lines 5640--5643
>\OT1/cmr/m/n/12 : Turns off any rewrite rules in the listed the-o-ries. As with
> \OT1/cmtt/m/n/12 auto-rewrite-theory[]\OT1/cmr/m/n/12 ,
>[101]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5661.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5674.
>Underfull \hbox (badness 10000) in paragraph at lines 5693--5695
>[]\OT1/cmr/m/n/12 : Adds the an-tecedent for-mula
>Overfull \hbox (9.57686pt too wide) in paragraph at lines 5702--5705
>[]\OT1/cmr/m/n/12 This means that there was
>[102]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5726.
>Underfull \hbox (badness 3049) in paragraph at lines 5755--5755
>[]|\OT1/cmr/m/n/12 Boolean/data ab-strac-tion fol-lowed by model-
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5763.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5763.
>[103]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5811.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5811.
>[104]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5862.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5862.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5905.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 5905.
>[105]
>Overfull \hbox (1.95076pt too wide) in paragraph at lines 5946--5950
>[]
>Overfull \hbox (14.11972pt too wide) in paragraph at lines 5951--5955
>[]\OT1/cmr/m/n/12 : In-vokes CTL/mu-calculus model
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5958.
>[106]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 5990.
>Overfull \hbox (8.12576pt too wide) in paragraph at lines 6022--6028
>[]\OT1/cmtt/m/n/12 "Skolemizing
>Overfull \hbox (12.70465pt too wide) in paragraph at lines 6036--6039
>[]\OT1/cmr/m/n/12 Applies the \OT1/cmtt/m/n/12 grind \OT1/cmr/m/n/12 strat-egy 
>but saves
>[107]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6052.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\char' on input line 6052.
>[108]
>Chapter 5.
>[109] [110]
>Overfull \hbox (9.0177pt too wide) in paragraph at lines 6188--6201
>\OT1/cmtt/m/n/12 binding-expr \OT1/cmr/m/n/12 with slots \OT1/cmtt/m/n/12 bindi
>ngs \OT1/cmr/m/n/12 which re-turns the bound vari-ables, and \OT1/cmtt/m/n/12 e
>xpression\OT1/cmr/m/n/12 ,
>[111] [112] [113] [114]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6381.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6399.
>[115]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6430.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6459.
>[116]
>Overfull \hbox (16.80458pt too wide) in paragraph at lines 6476--6477
>[]\OT1/cmtt/m/n/12 (try (try (skip) (assert) (fail)) (split) (flatten)) = (flat
>ten) 
>Overfull \hbox (10.62958pt too wide) in paragraph at lines 6478--6479
>[]\OT1/cmtt/m/n/12 (try (try (lemma "assoc") (fail) (assert)) (split) (flatten)
>) =
>Overfull \hbox (10.62958pt too wide) in paragraph at lines 6480--6481
>[]\OT1/cmtt/m/n/12 (try (try (lemma "assoc") (assert) (fail)) (split) (flatten)
>) =
>Overfull \hbox (26.75076pt too wide) in paragraph at lines 6497--6501
>[]\OT1/cmtt/m/n/12 (try (try (flatten) (fail) (skolem 1 ("a" "b"))) (postpone) 
>(prop))
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6514.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6528.
>[117]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6544.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6554.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6568.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6582.
>[118]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6600.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6611.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6651.
>[119]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6665.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6677.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6689.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6706.
>[120]
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6720.
>Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
>(hyperref)                removing `\largett' on input line 6740.
>(./prover.bbl (./prover.brf) [121] [122] [123]) (./prover.ind [124]
>Package relsize Warning: Font size 5.0pt is too small.
>(relsize)                Using 6.0pt instead on input line 17.
>Package relsize Warning: Font size 5.0pt is too small.
>(relsize)                Using 6.0pt instead on input line 17.
>Package relsize Warning: Font size 5.0pt is too small.
>(relsize)                Using 6.0pt instead on input line 17.
>Package relsize Warning: Font size 5.0pt is too small.
>(relsize)                Using 6.0pt instead on input line 17.
>Overfull \hbox (18.68642pt too wide) in paragraph at lines 17--19
>[]$\OT1/cmr/m/n/8 h\OML/cmm/m/it/8 A$\OT1/cmr/m/n/8 rulename$\OML/cmm/m/it/8 B$
> $\OT1/cmr/m/n/8 h\OML/cmm/m/it/8 A$\OT1/cmr/m/n/8 required$\OML/cmm/m/it/8 B$$
>[]$ \OT1/cmr/m/sc/6 &op-tional $\OT1/cmr/m/n/8 h\OML/cmm/m/it/8 A$\OT1/cmr/m/it
>/8 optional\OT1/cmr/m/n/8 [\OT1/cmtt/m/n/8 default\OT1/cmr/m/n/8 ]$\OML/cmm/m/i
>t/8 B$$[]$
>[125] [126] [127] [128]) (./prover.aux)
>LaTeX Font Warning: Some font shapes were not available, defaults substituted.
> )
>(see the transcript file for additional information)</usr/share/texlive/texmf-d
>ist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fo
>nts/type1/public/amsfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/fonts/typ
>e1/public/amsfonts/cm/cmbxti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
>ublic/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
>/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
>onts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
>m/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi
>6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb><
>/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/sh
>are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/tex
>live/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/te
>xmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/texmf-dis
>t/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/
>type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
>blic/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
>fonts/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
>cm/cmss17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cms
>y10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb
>></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr
>/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti12.pfb></usr/share
>/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texliv
>e/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texm
>f-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist
>/fonts/type1/public/amsfonts/cm/cmtt8.pfb>
>Output written on prover.pdf (136 pages, 707723 bytes).
>Transcript written on prover.log.
>make: Leaving directory '/builddir/build/BUILD/pvs-6.0/doc/prover'
>+ ps2pdf doc/user-guide/pvs-screen1.ps doc/user-guide/pvs-screen1.pdf
>+ touch doc/user-guide/user-guide.ind
>+ make -C doc/user-guide user-guide.pdf
>make: Entering directory '/builddir/build/BUILD/pvs-6.0/doc/user-guide'
>/builddir/build/BUILD/pvs-6.0/pvs -batch -q -l sum.el
>Loading /usr/share/emacs/site-lisp/site-start.d/autoconf-init.el (source)...
>Loading /usr/share/emacs/site-lisp/site-start.d/desktop-entry-mode-init.el (source)...
>error in process filter: Symbolâs value as variable is void: default-major-mode
>make: Leaving directory '/builddir/build/BUILD/pvs-6.0/doc/user-guide'
>make: *** [Makefile:32: sum-nosub.tex] Error 255
>RPM build errors:
>error: Bad exit status from /var/tmp/rpm-tmp.a3mExf (%build)
>    Bad exit status from /var/tmp/rpm-tmp.a3mExf (%build)
>Child return code was: 1
>EXCEPTION: [Error()]
>Traceback (most recent call last):
>  File "/usr/lib/python3.6/site-packages/mockbuild/trace_decorator.py", line 89, in trace
>    result = func(*args, **kw)
>  File "/usr/lib/python3.6/site-packages/mockbuild/util.py", line 582, in do
>    raise exception.Error("Command failed. See logs for output.\n # %s" % (command,), child.returncode)
>mockbuild.exception.Error: Command failed. See logs for output.
> # bash --login -c /usr/bin/rpmbuild -bb --target i686 --nodeps /builddir/build/SPECS/pvs-sbcl.spec

Actions: View

Attachments on bug 1605528: 1465764 | 1465765 | 1465766