Last active
February 23, 2020 12:30
-
-
Save catalin-hritcu/1db5104564906dfae727278eda778217 to your computer and use it in GitHub Desktop.
arXiv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| TeX log appears below | |
| [verbose]: Creating arXiv submission AutoTeX object | |
| [verbose]: *** Using TeX Live 2016 *** | |
| [verbose]: Calling arXiv submission AutoTeX process | |
| [verbose]: TeX/AutoTeX.pm: admin_timeout = minion | |
| [verbose]: <robust_diff_traces.tex> is of type 'TEX'. | |
| [verbose]: <instance-more-target-statements.tex> is of type 'TEX'. | |
| [verbose]: <expand-sec-diagram.tex> is of type 'TEX'. | |
| [verbose]: <diagram-prop-pres-comp-security.tex> is of type 'TEX'. | |
| [verbose]: <app-proofs-marco.tex> is of type 'TEX'. | |
| [verbose]: <rob-diff-acts.tex> is of type 'TEX'. | |
| [verbose]: <app-proofs-marco-statements.tex> is of type 'TEX'. | |
| [verbose]: <diff_traces.tex> is of type 'TEX'. | |
| [verbose]: <resource-exhaustion.tex> is of type 'TEX'. | |
| [verbose]: <diagram.tex> is of type 'TEX'. | |
| [verbose]: <diagram-sc-only.tex> is of type 'TEX'. | |
| [verbose]: <other_works.tex> is of type 'TEX'. | |
| [verbose]: <old-sc-diagram.tex> is of type 'TEX'. | |
| [verbose]: <ANI.tex> is of type 'TEX'. | |
| [verbose]: <coqed.sty> is of type 'TeX auxiliary'. | |
| [verbose]: <composition-appendix.tex> is of type 'TEX'. | |
| [verbose]: <early-failure.tex> is of type 'unknown'. | |
| [verbose]: <main.tex> is of type 'PDFLATEX'. | |
| [verbose]: <llncs.cls> is of type 'TeX auxiliary'. | |
| [verbose]: <diagram-rtc-only.tex> is of type 'TEX'. | |
| [verbose]: <diff_values.tex> is of type 'TEX'. | |
| [verbose]: <instance-marcodeepak.tex> is of type 'TEX'. | |
| [verbose]: <mappings.tex> is of type 'TEX'. | |
| [verbose]: <robust_diagram.tex> is of type 'TEX'. | |
| [verbose]: <main.bbl> is of type 'TeX auxiliary'. | |
| [verbose]: <prisc.tex> is of type 'PDFLATEX'. | |
| [verbose]: <instance-more-target.tex> is of type 'TEX'. | |
| [verbose]: <texdirectives.tex> is of type 'unknown'. | |
| [verbose]: <diagram-hc-only.tex> is of type 'TEX'. | |
| [verbose]: <abstract.tex> is of type 'unknown'. | |
| [verbose]: <sec-comp-explain.tex> is of type 'TEX'. | |
| [verbose]: <cc_by_4-0.eps> is of type 'Postscript'. | |
| [verbose]: <appendix-other.tex> is of type 'TEX'. | |
| [verbose]: <rob-pres-safety.tex> is of type 'unknown'. | |
| [verbose]: <coq.pdf> is of type 'PDF'. | |
| [verbose]: <rel_to_maps.tex> is of type 'TEX'. | |
| [verbose]: <instance-marco-inputs.tex> is of type 'TEX'. | |
| [verbose]: <appendixintro.tex> is of type 'unknown'. | |
| [verbose]: <undefbeh.tex> is of type 'TEX'. | |
| [verbose]: <rw-sec-crits-short.tex> is of type 'unknown'. | |
| [verbose]: <robust-trace.tex> is of type 'TEX'. | |
| [verbose]: <proofindex.tex> is of type 'TEX'. | |
| [verbose]: <criteria.tex> is of type 'TEX'. | |
| [verbose]: <two_dot_one.tex> is of type 'TEX'. | |
| [verbose]: <diagram-prop-pres-comp-corr.tex> is of type 'TEX'. | |
| [verbose]: <secure-compilation-motivation.tex> is of type 'TEX'. | |
| [verbose]: <diagram-cc-only.tex> is of type 'TEX'. | |
| [verbose]: <intro.tex> is of type 'TEX'. | |
| [verbose]: <relating_src_trg_traces.tex> is of type 'TEX'. | |
| [verbose]: <abbrvnaturl.bst> is of type 'TeX auxiliary'. | |
| [verbose]: <cmds.tex> is of type 'TEX'. | |
| [verbose]: ~~~~~~~~~~~ Processing file 'main.tex' | |
| [verbose]: arXiv Warning: user included plain hyperref directive. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running hpdflatex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && pdflatex 'main.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex) | |
| restricted \write18 enabled. | |
| entering extended mode | |
| (./main.tex | |
| LaTeX2e <2016/03/31> patch level 3 | |
| Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. | |
| (./texdirectives.tex) (./llncs.cls | |
| Document Class: llncs 2018/03/10 v2.20 | |
| LaTeX document class for Lecture Notes in Computer Science | |
| (/texlive/2016/texmf-dist/tex/latex/base/article.cls | |
| Document Class: article 2014/09/29 v1.4h Standard LaTeX document class | |
| (/texlive/2016/texmf-dist/tex/latex/base/size10.clo)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty | |
| (/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/times.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/dejavu/DejaVuSansMono.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/scalerel/scalerel.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tools/calc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-def/pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) | |
| (/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/wrapfig/wrapfig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/titlesec/titlesec.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/booktabs/booktabs.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/subcaption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption3.sty) | |
| Package caption Warning: Unsupported document class (or package) detected, | |
| (caption) usage of the caption package is not recommended. | |
| See the caption package documentation for explanation. | |
| )) (/texlive/2016/texmf-dist/tex/latex/semantic/semantic.sty | |
| Semantic Package v2.0(epsilon) [2003/10/28] | |
| CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ | |
| Loading features: | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, | |
| and general definitions. | |
| ) (/texlive/2016/texmf-dist/tex/latex/amsmath/amsmath.sty | |
| For additional information on amsmath, use the `?' option. | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amstext.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsgen.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsbsy.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsopn.sty) | |
| Package amsmath Warning: Unable to redefine math accent \vec. | |
| ) (/texlive/2016/texmf-dist/tex/latex/mathpartir/mathpartir.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/xspace.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/latexsym.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mathtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mhsetup.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/color.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.sty | |
| (/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/verbatim.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def | |
| (/texlive/2016/texmf-dist/tex/latex/ms/everyshi.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/dvipsnam.def)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.c | |
| ode.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex | |
| ) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmet | |
| ics.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code. | |
| tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.cod | |
| e.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex)) | |
| ) (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty | |
| )) (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgffor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/math/pgfmath.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arytopaths.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypositioning.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshadows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfadings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex) | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryarrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arycalc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arybackgrounds.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfit.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.geometric.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geo | |
| metric.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.misc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mis | |
| c.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.symbols.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.sym | |
| bols.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.arrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arr | |
| ows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.callouts.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.cal | |
| louts.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.multipart.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mul | |
| tipart.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.pathreplacing.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.pathreplacing.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypatterns.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.markings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.markings.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikzscale/tikzscale.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3packages/xparse/xparse.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3-code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/letltxmacro.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.tex))) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/t1enc.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/bera/beramono.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/epigraph/epigraph.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/float/float.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/refcount.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/gettitlestring.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/kvoptions.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/kvsetkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/etexcmds.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty)))))) | |
| (/texlive/2016/texmf-dist/tex/latex/changepage/changepage.sty) (./coqed.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/bm.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/cancel/cancel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/centernot.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-restate.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thmtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-patch.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/parseargs.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-kv.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-autoref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/aliasctr.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-listof.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-llncs.sty | |
| Package thmtools Warning: LLNCS support disables automatic casing of theorem na | |
| mes . | |
| ))) (/texlive/2016/texmf-dist/tex/latex/enumitem/enumitem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fancyvrb/fancyvrb.sty | |
| Style option: `fancyvrb' v2.7a, with DG/SPQR fixes, and firstline=lastline fix | |
| <2008/02/07> (tvz)) (/texlive/2016/texmf-dist/tex/latex/varwidth/varwidth.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/combelow/combelow.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/bussproofs/bussproofs.sty | |
| Proof Tree (bussproofs) style macros. Version 1.1. | |
| ) (/texlive/2016/texmf-dist/tex/generic/ulem/ulem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/yhmath/yhmath.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xy.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes, | |
| docmode, (/texlive/2016/texmf-dist/tex/generic/xypic/xyrecat.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyidioms.tex) | |
| Xy-pic version 3.8.9 <2013/10/06> | |
| Copyright (c) 1991-2013 by Kristoffer H. Rose <krisrose@tug.org> and others | |
| Xy-pic is free software: see the User's Guide for details. | |
| Loading kernel: messages; fonts; allocations: state, direction, | |
| utility macros; pictures: \xy, positions, objects, decorations; | |
| kernel objects: directionals, circles, text; options; algorithms: directions, | |
| edges, connections; Xy-pic loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ifpdf.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyall.tex | |
| Xy-pic option: All features v.3.8 | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycurve.tex | |
| Xy-pic option: Curve and Spline extension v.3.12 curve, circles, loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyframe.tex | |
| Xy-pic option: Frame and Bracket extension v.3.14 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycmtip.tex | |
| Xy-pic option: Computer Modern tip extension v.3.7 | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xytips.tex | |
| Xy-pic option: More Tips extension v.3.11 loaded) loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyline.tex | |
| Xy-pic option: Line styles extension v.3.10 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyrotate.tex | |
| Xy-pic option: Rotate and Scale extension v.3.8 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycolor.tex | |
| Xy-pic option: Colour extension v.3.11 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xymatrix.tex | |
| Xy-pic option: Matrix feature v.3.14 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyarrow.tex | |
| Xy-pic option: Arrow and Path feature v.3.9 path, \ar, loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xygraph.tex | |
| Xy-pic option: Graph feature v.3.11 loaded) loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf.tex | |
| Xy-pic option: PDF driver v.1.7 Xy-pic pdf driver: `color' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-co.tex loaded) | |
| Xy-pic pdf driver: `curve' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-cu.tex loaded) | |
| Xy-pic pdf driver: `frame' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-fr.tex loaded) | |
| Xy-pic pdf driver: `line' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-li.tex loaded) | |
| Xy-pic pdf driver: `rotate' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-ro.tex loaded) loaded)) | |
| (/texlive/2016/texmf-local/tex/latex/natbib/natbib.sty | |
| This is natbib version 8.31 | |
| ************************************************************* | |
| !!WARNING!! !!WARNING!! !!WARNING!! !!WARNING!! | |
| This version (v8.31) of natbib is stricter in its formatting | |
| requirements for bibitem entries than the previous version | |
| used at arXiv (v7.1). | |
| If your submission encounters a problem see | |
| http://arXiv.org/help/faq/texlive | |
| and the natbib documentation at | |
| http://www.ctan.org/tex-archive/macros/latex/contrib/natbib/ | |
| for explanation and adjust your submission accordingly. | |
| The arXiv team. | |
| ************************************************************* | |
| ) (/texlive/2016/texmf-dist/tex/latex/hyperref/hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/auxhook.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/pd1enc.def) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/hyperref.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/url/url.sty)) | |
| Package hyperref Message: Driver: hpdftex. | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/hpdftex.def | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/cleveref/cleveref.sty) (./cmds.tex) | |
| No file main.aux. | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/t1ptm.fd) | |
| (/texlive/2016/texmf-dist/tex/context/base/mkii/supp-pdf.mkii | |
| [Loading MPS to PDF converter (version 2006.09.02).] | |
| ) (/texlive/2016/texmf-dist/tex/latex/oberdiek/epstopdf-base.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/grfext.sty) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/epstopdf-sys.cfg)) | |
| ABD: EveryShipout initializing macros | |
| (/texlive/2016/texmf-dist/tex/latex/yhmath/OMXyhex.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ulasy.fd) | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\\' on input line 524. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 524. | |
| (./abstract.tex) (./intro.tex | |
| Package natbib Warning: Citation `McCarthyP67' on page 1 undefined on input lin | |
| e 13. | |
| Package natbib Warning: Citation `MilnerW72' on page 1 undefined on input line | |
| 13. | |
| Package natbib Warning: Citation `Morris73a' on page 1 undefined on input line | |
| 13. | |
| Package natbib Warning: Citation `Leroy09' on page 1 undefined on input line 17 | |
| . | |
| Package natbib Warning: Citation `SevcikVNJS13' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `MullenZTG16' on page 1 undefined on input lin | |
| e 20. | |
| Package natbib Warning: Citation `StewartBCA15' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `KangKHDV15' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `KangHMGZV15' on page 1 undefined on input lin | |
| e 20. | |
| Package natbib Warning: Citation `BessonBW19' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `WangWS19' on page 1 undefined on input line 2 | |
| 0. | |
| Package natbib Warning: Citation `GuSKWKS0CR18' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `RamananandroSWKF15' on page 1 undefined on in | |
| put line 20. | |
| Package natbib Warning: Citation `CarbonneauxHRS14' on page 1 undefined on inpu | |
| t line 20. | |
| Package natbib Warning: Citation `BoldoJLM15' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `ZhaoNMZ12' on page 1 undefined on input line | |
| 23. | |
| Package natbib Warning: Citation `NeisHKMDV15' on page 1 undefined on input lin | |
| e 24. | |
| Package natbib Warning: Citation `TanMKFON19' on page 1 undefined on input line | |
| 25. | |
| Package natbib Warning: Citation `CertiCoq17' on page 1 undefined on input line | |
| 27. | |
| Package natbib Warning: Citation `SecureCompilationSIGPLAN19' on page 1 undefin | |
| ed on input line 48. | |
| Package natbib Warning: Citation `dagstuhl-sc-2018' on page 1 undefined on inpu | |
| t line 48. | |
| Package natbib Warning: Citation `Leroy09' on page 1 undefined on input line 66 | |
| . | |
| Package natbib Warning: Citation `TanMKFON19' on page 1 undefined on input line | |
| 67. | |
| [1{/texlive/2016/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 78 | |
| . | |
| LaTeX Warning: Reference `sec:secure-compilation' on page 2 undefined on input | |
| line 142. | |
| Package natbib Warning: Citation `patrignani2020use' on page 2 undefined on inp | |
| ut line 152. | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 18 | |
| 2. | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 18 | |
| 4. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 1 | |
| 87. | |
| Package natbib Warning: Citation `Heartbleed' on page 2 undefined on input line | |
| 201. | |
| Package natbib Warning: Citation `memory-unsafety' on page 2 undefined on input | |
| line 201. | |
| Package natbib Warning: Citation `HallerJPPGBK16' on page 2 undefined on input | |
| line 201. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 02. | |
| Package natbib Warning: Citation `Lattner11' on page 2 undefined on input line | |
| 202. | |
| Package natbib Warning: Citation `WangZKS13' on page 2 undefined on input line | |
| 202. | |
| Package natbib Warning: Citation `WangCCJZK12' on page 2 undefined on input lin | |
| e 202. | |
| (/texlive/2016/texmf-dist/tex/latex/bera/t1fvm.fd) | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 08. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 12. | |
| Package natbib Warning: Citation `TanMKFON19' on page 2 undefined on input line | |
| 218. | |
| [2] | |
| LaTeX Warning: Reference `def:bcc' on page 3 undefined on input line 268. | |
| [3] | |
| Package natbib Warning: Citation `LamportS84' on page 4 undefined on input line | |
| 432. | |
| LaTeX Font Warning: Font shape `U/stmry/b/n' undefined | |
| (Font) using `U/stmry/m/n' instead on input line 440. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 4 undefined on | |
| input line 511. | |
| Package natbib Warning: Citation `backhouse2004safety' on page 4 undefined on i | |
| nput line 511. | |
| Package natbib Warning: Citation `naumann1998categorical' on page 4 undefined o | |
| n input line 511. | |
| LaTeX Warning: Reference `fig:diagram-cc' on page 4 undefined on input line 571 | |
| . | |
| (./diagram-cc-only.tex) [4] | |
| LaTeX Warning: Reference `sec:trinity' on page 5 undefined on input line 628. | |
| LaTeX Warning: Reference `fig:diagram-cc' on page 5 undefined on input line 629 | |
| . | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 5 undefined on | |
| input line 641. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 5 undefined on input line | |
| 643. | |
| LaTeX Warning: Reference `sec:example-undef' on page 5 undefined on input line | |
| 732. | |
| LaTeX Warning: Reference `sec:example-resources' on page 5 undefined on input l | |
| ine 733. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 5 undefined on input | |
| line 734. | |
| LaTeX Warning: Reference `sec:example-split-io' on page 5 undefined on input li | |
| ne 736. | |
| Package natbib Warning: Citation `GoguenM82' on page 5 undefined on input line | |
| 758. | |
| LaTeX Warning: Reference `sec:example-noninterference' on page 5 undefined on i | |
| nput line 761. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 5 undefined o | |
| n input line 764. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 5 undefined on input li | |
| ne 799. | |
| LaTeX Warning: Reference `sec:secure-compilation' on page 5 undefined on input | |
| line 801. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 5 undefined on input li | |
| ne 811. | |
| LaTeX Warning: Reference `sec:related' on page 5 undefined on input line 823. | |
| LaTeX Warning: Reference `sec:conclusion' on page 5 undefined on input line 823 | |
| . | |
| <coq.pdf, id=93, 449.06996pt x 553.30359pt> <use coq.pdf>) | |
| LaTeX Warning: Reference `sec:correct-trace-props' on page 5 undefined on input | |
| line 638. | |
| LaTeX Warning: Reference `thm:galois' on page 5 undefined on input line 642. | |
| LaTeX Warning: Reference `sec:trinity' on page 5 undefined on input line 672. | |
| Package natbib Warning: Citation `ClarksonS10' on page 5 undefined on input lin | |
| e 682. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 5 undefined on input line | |
| 687. | |
| Underfull \vbox (badness 5105) has occurred while \output is active [5 <./coq.p | |
| df>] | |
| LaTeX Warning: Reference `sec:intro' on page 6 undefined on input line 739. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.1} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.758 \begin{definition} | |
| [\tpsigma and \tptau] \label{defn:TP} | |
| Package natbib Warning: Citation `CousotCousot77-1' on page 6 undefined on inpu | |
| t line 798. | |
| Package natbib Warning: Citation `Melton:1986' on page 6 undefined on input lin | |
| e 798. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.2} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.800 \begin{definition} | |
| [Galois connection] Let $(X, \preceq)$ and | |
| Overfull \hbox (4.70688pt too wide) in paragraph at lines 819--822 | |
| []\T1/ptm/b/n/10 (Characteristic prop-erty of Ga-lois con-nec-tions). [][]\T1/p | |
| tm/m/it/10 If $\OML/cmm/m/it/10 []\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 X; \OMS/cm | |
| sy/m/n/10 ^^V\OT1/cmr/m/n/10 ) \U/msa/m/n/10 ^^\ []$ | |
| [6] | |
| LaTeX Warning: Reference `lem:chG' on page 7 undefined on input line 836. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `lem:correspond' on page 7 undefined on input line 872 | |
| . | |
| LaTeX Warning: Reference `thm:correspondcriteria' on page 7 undefined on input | |
| line 873. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 7 undefined on input l | |
| ine 883. | |
| Package natbib Warning: Citation `TanMKFON19' on page 7 undefined on input line | |
| 883. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 7 undefined on | |
| input line 885. | |
| LaTeX Warning: Reference `defn:TP' on page 7 undefined on input line 898. | |
| LaTeX Warning: Reference `sec:intro' on page 7 undefined on input line 899. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:galois' on page 7 undefined on input line 908. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:correspondcriteria' on page 7 undefined on input | |
| line 911. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 7 undefined on | |
| input line 943. | |
| <use coq.pdf> [7] | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 1000. | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 1013. | |
| LaTeX Warning: Reference `lem:correspond' on page 8 undefined on input line 101 | |
| 6. | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 1018. | |
| LaTeX Warning: Reference `sec:example-resources' on page 8 undefined on input l | |
| ine 1047. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1112. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1115. | |
| LaTeX Warning: Reference `thm:ssch' on page 8 undefined on input line 1122. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1129. | |
| LaTeX Warning: Reference `sec:trinity' on page 8 undefined on input line 1156. | |
| [8] | |
| Package natbib Warning: Citation `mastroeni2018verifying' on page 9 undefined o | |
| n input line 1177. | |
| Package natbib Warning: Citation `naumann2019whither' on page 9 undefined on in | |
| put line 1177. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:ssch' on page 9 undefined on input line 1205. | |
| LaTeX Warning: Reference `sec:example-noninterference' on page 9 undefined on i | |
| nput line 1208. | |
| LaTeX Warning: Reference `sec:example-undef' on page 9 undefined on input line | |
| 1224. | |
| LaTeX Warning: Reference `sec:example-resources' on page 9 undefined on input l | |
| ine 1228. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 9 undefined on input | |
| line 1230. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 9 undefined on input line | |
| 1233. | |
| (./undefbeh.tex | |
| LaTeX Warning: Reference `sec:intro' on page 9 undefined on input line 3. | |
| LaTeX Warning: Reference `sec:intro' on page 9 undefined on input line 49. | |
| <use coq.pdf> [9] | |
| Package natbib Warning: Citation `CaoBGDA18' on page 10 undefined on input line | |
| 165. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 10 undefined on input li | |
| ne 182. | |
| ) (./resource-exhaustion.tex | |
| LaTeX Warning: Reference `sec:intro' on page 10 undefined on input line 4. | |
| <use coq.pdf> [10] | |
| Package natbib Warning: Citation `LamportS84' on page 11 undefined on input lin | |
| e 107. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `sec:safety-preservation' on page 11 undefined on inpu | |
| t line 115. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 11 undefined on inpu | |
| t line 153. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `DeepSpecLeroy' on page 11 undefined on input | |
| line 171. | |
| ) (./diff_values.tex <use coq.pdf> [11] | |
| LaTeX Warning: Reference `tr:ste-con' on page 1 undefined on input line 127. | |
| LaTeX Warning: Reference `tr:ste-em' on page 1 undefined on input line 127. | |
| LaTeX Warning: Reference `tr:ste-b' on page 1 undefined on input line 128. | |
| LaTeX Warning: Reference `tr:ste-n' on page 1 undefined on input line 128. | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/t1phv.fd) <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-dv-cc' on page 12 undefined on input line 20 | |
| 9. | |
| Package natbib Warning: Citation `Engelfriet85' on page 12 undefined on input l | |
| ine 214. | |
| Package natbib Warning: Citation `milner82' on page 12 undefined on input line | |
| 214. | |
| Package natbib Warning: Citation `ZakinthinosL97' on page 12 undefined on input | |
| line 215. | |
| Package natbib Warning: Citation `FocardiG95' on page 12 undefined on input lin | |
| e 215. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 12 undefined on input | |
| line 218. | |
| Package natbib Warning: Citation `Leroy09b' on page 12 undefined on input line | |
| 218. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 12 undefined on input | |
| line 225. | |
| Package natbib Warning: Citation `Leroy09b' on page 12 undefined on input line | |
| 225. | |
| <xymatrix 5x3 458> [12] <xymatrix 5x2 386> <use coq.pdf> | |
| Package natbib Warning: Citation `BeringerSDA14' on page 13 undefined on input | |
| line 320. | |
| Package natbib Warning: Citation `Leroy09b' on page 13 undefined on input line | |
| 320. | |
| ) (./instance-more-target-statements.tex | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 13 undefined on inpu | |
| t line 14. | |
| [13] | |
| LaTeX Warning: Reference `tr:tr-rel-n' on page 1 undefined on input line 113. | |
| LaTeX Warning: Reference `tr:tr-rel-m-m' on page 1 undefined on input line 115. | |
| LaTeX Warning: Reference `tr:tr-rel-m-n' on page 1 undefined on input line 115. | |
| LaTeX Warning: Reference `tr:tr-rel-n-m' on page 1 undefined on input line 115. | |
| Underfull \hbox (badness 10000) in paragraph at lines 112--140 | |
| \T1/ptm/m/n/10 build on these rules to de-fine the | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 14 undefined on input line | |
| 142. | |
| LaTeX Warning: Reference `tr:tr-rel-full' on page 1 undefined on input line 149 | |
| . | |
| ) (./ANI.tex | |
| Package natbib Warning: Citation `GoguenM82' on page 14 undefined on input line | |
| 16. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 14 undefined on input line | |
| 17. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 14 undefined | |
| on input line 52. | |
| [14] | |
| LaTeX Warning: Reference `thm:ssch' on page 15 undefined on input line 239. | |
| [15] | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 267. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 386. | |
| Package natbib Warning: Citation `CousotCousot77-1' on page 16 undefined on inp | |
| ut line 388. | |
| Package natbib Warning: Citation `sabelfeld05:_dimensions_declass' on page 16 u | |
| ndefined on input line 392. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 447. | |
| [16] | |
| LaTeX Warning: Reference `thm:compilingANI' on page 17 undefined on input line | |
| 618. | |
| LaTeX Warning: Reference `sec:trinity' on page 17 undefined on input line 673. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 58. | |
| LaTeX Warning: Reference `sec:instances' on page 17 undefined on input line 759 | |
| . | |
| LaTeX Warning: Reference `sec:example-undef' on page 17 undefined on input line | |
| 760. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 85. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 94. | |
| [17] | |
| LaTeX Warning: Reference `thm:genANI' on page 1 undefined on input line 842. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 18 undefined | |
| on input line 844. | |
| Package natbib Warning: Citation `AbadiCCD' on page 18 undefined on input line | |
| 874. | |
| Package natbib Warning: Citation `mastroeni2018verifying' on page 18 undefined | |
| on input line 874. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 18 undefined on input lin | |
| e 883. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 18 undefined on input lin | |
| e 885. | |
| Overfull \hbox (15.32541pt too wide) in paragraph at lines 922--927 | |
| []\T1/ptm/b/n/10 (Target ANI by source ANI). [][]\T1/ptm/m/it/10 Let $[][] \OMS | |
| /cmsy/m/n/10 2 []\OT1/cmr/m/n/10 (2[])$\T1/ptm/m/it/10 , $[][] \OMS/cmsy/m/n/10 | |
| 2 []\OT1/cmr/m/n/10 (2[])$ | |
| Package natbib Warning: Citation `BartheGL18' on page 18 undefined on input lin | |
| e 1045. | |
| Package natbib Warning: Citation `DSilvaPS15' on page 18 undefined on input lin | |
| e 1045. | |
| ) (./secure-compilation-motivation.tex [18] | |
| Package natbib Warning: Citation `Leroy09' on page 19 undefined on input line 2 | |
| 8. | |
| Package natbib Warning: Citation `NeisHKMDV15' on page 19 undefined on input li | |
| ne 33. | |
| Package natbib Warning: Citation `StewartBCA15' on page 19 undefined on input l | |
| ine 33. | |
| Package natbib Warning: Citation `HurD11' on page 19 undefined on input line 33 | |
| . | |
| Package natbib Warning: Citation `KangKHDV15' on page 19 undefined on input lin | |
| e 33. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 39. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 96. | |
| LaTeX Warning: Reference `sec:compiler-correctness' on page 19 undefined on inp | |
| ut line 107. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 113. | |
| LaTeX Warning: Reference `sec:sec-comp-trini' on page 19 undefined on input lin | |
| e 117. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 19 undefined on input li | |
| ne 125. | |
| LaTeX Warning: Reference `sec:comp-summ' on page 19 undefined on input line 126 | |
| . | |
| ) (./sec-comp-explain.tex | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 10. | |
| LaTeX Warning: Reference `sec:compiler-correctness' on page 19 undefined on inp | |
| ut line 11. | |
| LaTeX Warning: Reference `thm:rtc-trinity' on page 1 undefined on input line 20 | |
| . | |
| [19] <use coq.pdf>) (./expand-sec-diagram.tex | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 20 undefined on input l | |
| ine 2. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 20 undefined on input l | |
| ine 37. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 20 undefined | |
| on input line 42. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `ClarksonS10' on page 20 undefined on input li | |
| ne 91. | |
| LaTeX Warning: Reference `thm:ssch' on page 20 undefined on input line 94. | |
| [20] <use coq.pdf> <use coq.pdf> | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 21 undefined | |
| on input line 119. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 21 undefined | |
| on input line 173. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 1 undefined o | |
| n input line 213. | |
| (./diagram-prop-pres-comp-security.tex <use coq.pdf> <use coq.pdf> | |
| <use coq.pdf> <use coq.pdf> <use coq.pdf> <use coq.pdf> <use coq.pdf> | |
| <use coq.pdf> <use coq.pdf>)) (./robust-trace.tex [21] | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 22 undefined on inpu | |
| t line 19. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 22 undefined on inpu | |
| t line 145. | |
| Underfull \vbox (badness 2443) has occurred while \output is active [22] | |
| <use coq.pdf>) (./rw-sec-crits-short.tex | |
| Package natbib Warning: Citation `PatrignaniG18' on page 23 undefined on input | |
| line 6. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 23 undefined on inpu | |
| t line 7. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 23 undefined on input | |
| line 19. | |
| ) [23] | |
| Package natbib Warning: Citation `Leroy09' on page 24 undefined on input line 1 | |
| 353. | |
| Package natbib Warning: Citation `TanMKFON19' on page 24 undefined on input lin | |
| e 1353. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 24 undefined on input l | |
| ine 1354. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 24 undefined on input | |
| line 1354. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 24 undefined on input | |
| line 1354. | |
| LaTeX Warning: Reference `thm:rsp-sec-trinity' on page 24 undefined on input li | |
| ne 1360. | |
| Package natbib Warning: Citation `ClarksonS10' on page 24 undefined on input li | |
| ne 1363. | |
| Package natbib Warning: Citation `PasquaM17' on page 24 undefined on input line | |
| 1365. | |
| Package natbib Warning: Citation `XiaZHHMPZ20' on page 24 undefined on input li | |
| ne 1370. | |
| Package natbib Warning: Citation `XiaZHHMPZ20' on page 24 undefined on input li | |
| ne 1372. | |
| Package natbib Warning: Citation `WangWS19' on page 24 undefined on input line | |
| 1403. | |
| LaTeX Warning: Reference `sec:example-undef' on page 24 undefined on input line | |
| 1405. | |
| Package natbib Warning: Citation `SevcikVNJS13' on page 24 undefined on input l | |
| ine 1408. | |
| Package natbib Warning: Citation `KangHMGZV15' on page 24 undefined on input li | |
| ne 1408. | |
| Package natbib Warning: Citation `CarbonneauxHRS14' on page 24 undefined on inp | |
| ut line 1408. | |
| Package natbib Warning: Citation `MullenZTG16' on page 24 undefined on input li | |
| ne 1408. | |
| Package natbib Warning: Citation `TanMKFON19' on page 24 undefined on input lin | |
| e 1408. | |
| LaTeX Warning: Reference `sec:example-resources' on page 24 undefined on input | |
| line 1410. | |
| Package natbib Warning: Citation `HurD11' on page 24 undefined on input line 14 | |
| 58. | |
| Package natbib Warning: Citation `JeffreyR05' on page 24 undefined on input lin | |
| e 1471. | |
| Package natbib Warning: Citation `PatrignaniC15' on page 24 undefined on input | |
| line 1471. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 24 undefined on input l | |
| ine 1471. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 24 undefined | |
| on input line 1475. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1504. | |
| LaTeX Warning: Reference `fig:morris' on page 24 undefined on input line 1507. | |
| Package natbib Warning: Citation `PattersonA19' on page 24 undefined on input l | |
| ine 1510. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1513. | |
| Overfull \hbox (19.37321pt too wide) in paragraph at lines 1536--1537 | |
| [][] | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1558. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1558. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1558. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1558. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1558. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1558. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1558. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1558. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1558. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1558. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1558. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1558. | |
| [24] | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1565. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1565. | |
| LaTeX Warning: Reference `fig:morris' on page 25 undefined on input line 1566. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1567. | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1567. | |
| Package natbib Warning: Citation `cousot2002constructive' on page 25 undefined | |
| on input line 1581. | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1582. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1582. | |
| LaTeX Warning: Reference `sec:relatedwork' on page 25 undefined on input line 1 | |
| 583. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 25 undefined on input l | |
| ine 1605. | |
| Package natbib Warning: Citation `BusiDG19' on page 25 undefined on input line | |
| 1605. | |
| LaTeX Warning: Reference `sec:intro' on page 25 undefined on input line 1679. | |
| (./appendixintro.tex [25] | |
| LaTeX Warning: Reference `sec:pi' on page 1 undefined on input line 5. | |
| LaTeX Warning: Reference `sec:other-classes' on page 1 undefined on input line | |
| 9. | |
| Package natbib Warning: Citation `Melton:1986' on page 26 undefined on input li | |
| ne 11. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 26 undefined on | |
| input line 12. | |
| LaTeX Warning: Reference `sec:relatedwork' on page 1 undefined on input line 12 | |
| . | |
| LaTeX Warning: Reference `sec:instances' on page 1 undefined on input line 14. | |
| LaTeX Warning: Reference `sec:elided' on page 1 undefined on input line 15. | |
| LaTeX Warning: Reference `sec:composition' on page 1 undefined on input line 18 | |
| . | |
| LaTeX Warning: Reference `sec:in-depth-trsec' on page 1 undefined on input line | |
| 21. | |
| ) (./proofindex.tex | |
| LaTeX Warning: Reference `thm:galois' on page 26 undefined on input line 5. | |
| <use coq.pdf> | |
| Overfull \hbox (0.30478pt too wide) in paragraph at lines 5--17 | |
| \T1/ptm/m/n/10 ($\OMS/cmsy/m/n/10 ($\T1/ptm/m/n/10 ) As-sume $[]$ and that $[]$ | |
| sat-is-fies $[] \OMS/cmsy/m/n/10 ^^R \OML/cmm/m/it/10 ^^[\OT1/cmr/m/n/10 (\OML | |
| /cmm/m/it/10 ^^\\OT1/cmr/m/n/10 ([]))$\T1/ptm/m/n/10 . Ap-ply $[]$ to $[]$ and | |
| $\OML/cmm/m/it/10 ^^[\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 ^^\\OT1/cmr/m/n/10 ([])) | |
| $ | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 26 undefined on input li | |
| ne 24. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:galois' on page 26 undefined on input line 27. | |
| Overfull \hbox (2.1672pt too wide) in paragraph at lines 24--28 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 See The-o-rems rel_TC_$\OML/cmm | |
| /m/it/10 ^^\$\T1/ptm/m/n/10 TP and rel_TC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 | |
| TP in \T1/fvm/m/n/10 TraceCriterion.v | |
| LaTeX Warning: Reference `lem:surj_rel' on page 26 undefined on input line 44. | |
| LaTeX Warning: Reference `thm:ssch' on page 26 undefined on input line 109. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-dv-cc' on page 26 undefined on input line 11 | |
| 6. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 26 undefined on input line | |
| 121. | |
| LaTeX Warning: Reference `sec:proofs-marco' on page 26 undefined on input line | |
| 122. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 26 undefined on input line | |
| 126. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 138. | |
| [26] | |
| LaTeX Warning: Reference `thm:genANI' on page 27 undefined on input line 197. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 211. | |
| Underfull \hbox (badness 10000) in paragraph at lines 197--216 | |
| [27] | |
| Underfull \hbox (badness 10000) in paragraph at lines 227--230 | |
| LaTeX Warning: Reference `thm:srcANI' on page 28 undefined on input line 238. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 251. | |
| Underfull \hbox (badness 10000) in paragraph at lines 238--256 | |
| LaTeX Warning: Reference `thm:rtc-trinity' on page 28 undefined on input line 2 | |
| 78. | |
| <use coq.pdf> | |
| Overfull \hbox (42.58676pt too wide) in paragraph at lines 278--280 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems rel_RTC_$\OML/cmm/m/ | |
| it/10 ^^\$\T1/ptm/m/n/10 RTP and rel_RTC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 R | |
| TP in \T1/fvm/m/n/10 RobustTraceCriterion.v\T1/ptm/m/n/10 . | |
| LaTeX Warning: Reference `thm:rsp-sec-trinity' on page 28 undefined on input li | |
| ne 283. | |
| <use coq.pdf> | |
| Overfull \hbox (76.64267pt too wide) in paragraph at lines 283--285 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems tilde_RSC_$\OML/cmm/ | |
| m/it/10 ^^[$\T1/ptm/m/n/10 RSP and tilde_RSC_Cl_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m | |
| /n/10 RTP in \T1/fvm/m/n/10 RobustSafetyCriterion.v\T1/ptm/m/n/10 . | |
| LaTeX Warning: Reference `thm:rhp-sec-trinity' on page 28 undefined on input li | |
| ne 288. | |
| <use coq.pdf> | |
| Overfull \hbox (42.74326pt too wide) in paragraph at lines 288--290 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 Lem-mas $\OML/cmm/m/it/10 ^^[$\ | |
| T1/ptm/m/n/10 RHP_rel_RHC and rel_RHC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 RHP | |
| and The-o-rem rel_RHC_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m/n/10 RHP | |
| LaTeX Warning: Reference `thm:rob' on page 28 undefined on input line 293. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 28 undefined on input l | |
| ine 302. | |
| Package natbib Warning: Citation `MarcosSurvey' on page 28 undefined on input l | |
| ine 302. | |
| Package natbib Warning: Citation `Ahmed:2016:ICFP:UnivEmb' on page 28 undefined | |
| on input line 302. | |
| Package natbib Warning: Citation `skorstengaard-stktokens:2019' on page 28 unde | |
| fined on input line 302. | |
| LaTeX Warning: Reference `thm:trini-safe' on page 28 undefined on input line 33 | |
| 6. | |
| <use coq.pdf> | |
| Overfull \hbox (20.5833pt too wide) in paragraph at lines 336--339 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems tilde_SC_$\OML/cmm/m | |
| /it/10 ^^[$\T1/ptm/m/n/10 SP and tilde_SC_Cl_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m/n/ | |
| 10 TP in \T1/fvm/m/n/10 SafetyCriterion.v\T1/ptm/m/n/10 . | |
| [28] | |
| LaTeX Warning: Reference `thm:eq-hp' on page 29 undefined on input line 343. | |
| LaTeX Warning: Reference `thm:wktr' on page 29 undefined on input line 353. | |
| <use coq.pdf> | |
| Overfull \hbox (49.34982pt too wide) in paragraph at lines 353--355 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems rel_HC_$\OML/cmm/m/i | |
| t/10 ^^\$\T1/ptm/m/n/10 HP, rel_HC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 HP and | |
| $\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 HP_rel_HC in \T1/fvm/m/n/10 HyperCriterion | |
| .v\T1/ptm/m/n/10 . | |
| ) (./appendix-other.tex | |
| LaTeX Warning: Reference `sec:safety-preservation' on page 29 undefined on inpu | |
| t line 15. | |
| LaTeX Warning: Reference `sec:correct-hyper' on page 29 undefined on input line | |
| 17. | |
| Package natbib Warning: Citation `ClarksonS10' on page 29 undefined on input li | |
| ne 43. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.1} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.56 \begin{definition} | |
| [Safety Properties] | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 29 undefined on input l | |
| ine 90. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.2} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.100 \begin{definition} | |
| [$\sctilde$] | |
| LaTeX Warning: Reference `sec:subset-closed' on page 29 undefined on input line | |
| 114. | |
| [29] | |
| Overfull \hbox (4.73111pt too wide) in paragraph at lines 126--129 | |
| []\T1/ptm/b/n/10 (Trinitarian view for Safety). [][]\T1/ptm/m/it/10 For a trace | |
| re-la-tion $\OMS/cmsy/m/n/10 ^^X ^^R [] ^^B []$ | |
| Overfull \hbox (10.21405pt too wide) in paragraph at lines 136--136 | |
| [] | |
| (./diagram-sc-only.tex) | |
| Overfull \hbox (17.11406pt too wide) in paragraph at lines 130--143 | |
| [] $[]$ $[]$ | |
| Package natbib Warning: Citation `ClarksonS10' on page 30 undefined on input li | |
| ne 179. | |
| (./diagram-hc-only.tex) | |
| Overfull \hbox (16.90001pt too wide) in paragraph at lines 241--255 | |
| []$[]$ $[]$ | |
| [30] | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-cc' on page 31 undefined o | |
| n input line 257. | |
| (./diagram-prop-pres-comp-corr.tex)) (./other_works.tex | |
| Package natbib Warning: Citation `Melton:1986' on page 31 undefined on input li | |
| ne 102. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 31 undefined on | |
| input line 103. | |
| Package natbib Warning: Citation `Melton:1986' on page 31 undefined on input li | |
| ne 104. | |
| ) (./app-proofs-marco-statements.tex | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 1 undefined on input | |
| line 4. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 4. | |
| Overfull \hbox (4.3616pt too wide) in paragraph at lines 35--35 | |
| [] | |
| [31] <use coq.pdf> | |
| LaTeX Warning: Reference `tr:sem-nat' on page 1 undefined on input line 180. | |
| LaTeX Warning: Reference `tr:sem-in-nat' on page 1 undefined on input line 180. | |
| LaTeX Warning: Reference `tr:sem-s-nat' on page 1 undefined on input line 180. | |
| Overfull \hbox (29.37361pt too wide) in paragraph at lines 253--253 | |
| [] | |
| [32] | |
| LaTeX Warning: Reference `SEC:M' on page 1 undefined on input line 259. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 259. | |
| Overfull \hbox (40.73592pt too wide) in paragraph at lines 287--287 | |
| [] | |
| [33] | |
| Overfull \hbox (30.26236pt too wide) in paragraph at lines 550--550 | |
| [] | |
| LaTeX Warning: Reference `SEC:M' on page 1 undefined on input line 573. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 573. | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 1 undefined on input line | |
| 574. | |
| LaTeX Warning: Reference `thm:inst-marco-gensend' on page 1 undefined on input | |
| line 575. | |
| LaTeX Warning: Reference `thm:inst-marco-cc-expr' on page 1 undefined on input | |
| line 576. | |
| pdfTeX warning (ext4): destination with the same identifier (name{lemma.1}) has | |
| been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.580 \begin{lemma} | |
| [\gensends{\cdot} works]\label{thm:inst-marco-gensend} | |
| Overfull \hbox (58.24623pt too wide) in paragraph at lines 580--587 | |
| []\T1/ptm/b/n/10 ($[]$ works). [][]$[][][][][][] [] []$ | |
| Overfull \hbox (2.40167pt too wide) in paragraph at lines 595--596 | |
| []$[]$ \T1/ptm/m/n/10 trans-lates that into $[]$. | |
| LaTeX Warning: Reference `tr:e-tm-send' on page 1 undefined on input line 597. | |
| [34] | |
| LaTeX Warning: Reference `tr:tr-rel-n' on page 1 undefined on input line 602. | |
| Overfull \hbox (8.17157pt too wide) in paragraph at lines 619--619 | |
| [] | |
| Overfull \hbox (16.16049pt too wide) in paragraph at lines 621--632 | |
| []\T1/ptm/m/n/10 By as-sump-tion we have HP1 $[]$ | |
| LaTeX Warning: Reference `tr:tr-rel-m-m' on page 1 undefined on input line 649. | |
| LaTeX Warning: Reference `tr:tr-rel-n-m' on page 1 undefined on input line 657. | |
| LaTeX Warning: Reference `tr:tr-rel-m-n' on page 1 undefined on input line 661. | |
| Overfull \hbox (19.9337pt too wide) in paragraph at lines 667--673 | |
| []\T1/ptm/b/n/10 ($[][]$ is cor-rect for ex-pres-sions). [][]$[][][][]$ | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 35 undefined on input line | |
| 681. | |
| LaTeX Warning: Reference `thm:inst-marco-cc-expr' on page 35 undefined on input | |
| line 697. | |
| LaTeX Warning: Reference `thm:inst-marco-gensend' on page 35 undefined on input | |
| line 703. | |
| LaTeX Warning: Reference `tr:es-sm-send' on page 1 undefined on input line 708. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 1 undefined on input lin | |
| e 718. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 718. | |
| Overfull \hbox (10.78104pt too wide) in paragraph at lines 750--750 | |
| [] | |
| ) (./composition-appendix.tex [35] | |
| LaTeX Warning: Reference `sec:trinity' on page 1 undefined on input line 44. | |
| ) | |
| LaTeX Warning: Reference `sec:comp-summ' on page 36 undefined on input line 182 | |
| 0. | |
| (./rob-pres-safety.tex | |
| Package natbib Warning: Citation `patrignani_thesis' on page 36 undefined on in | |
| put line 15. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 36 undefined on input | |
| line 15. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 36 undefined on input l | |
| ine 15. | |
| Package natbib Warning: Citation `JuglaretHAEP16' on page 36 undefined on input | |
| line 15. | |
| Package natbib Warning: Citation `JeffreyR05' on page 36 undefined on input lin | |
| e 17. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 36 undefined on input | |
| line 22. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 36 undefined | |
| on input line 24. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 1 undefined on input lin | |
| e 30. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 1 undefined on input line | |
| 30. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 1 undefined on input | |
| line 30. | |
| Package natbib Warning: Citation `Schneider00' on page 36 undefined on input li | |
| ne 35. | |
| [36] | |
| Package natbib Warning: Citation `MarcosSurvey' on page 37 undefined on input l | |
| ine 51. | |
| Package natbib Warning: Citation `Leroy09b' on page 37 undefined on input line | |
| 51. | |
| ) (./instance-marcodeepak.tex | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 32. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 41. | |
| Overfull \hbox (15.95178pt too wide) in paragraph at lines 98--98 | |
| [] | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 99. | |
| ) (./main.bbl [37] [38] [39]) | |
| Underfull \hbox (badness 4699) in paragraph at lines 1857--1858 | |
| \T1/ptm/b/n/9 Open Ac-cess \T1/ptm/m/n/9 This chap-ter is li-censed un-der the | |
| terms of the Cre-ative Com-mons | |
| Overfull \hbox (10.0886pt too wide) in paragraph at lines 1857--1858 | |
| \T1/ptm/m/n/9 Attribution 4.0 In-ter-na-tional Li-cense ([][]$\T1/fvm/m/n/9 htt | |
| p : / / creativecommons . org / licenses / by / 4 . 0/$[][]\T1/ptm/m/n/9 ), whi | |
| ch | |
| Underfull \hbox (badness 10000) in paragraph at lines 1859--1860 | |
| \T1/ptm/m/n/9 cluded in the chap-ter's Cre-ative Com-mons li-cense and your in- | |
| tended | |
| ! Package pdftex.def Error: File `cc_by_4-0.pdf' not found. | |
| See the pdftex.def package documentation for explanation. | |
| Type H <return> for immediate help. | |
| ... | |
| l.1861 ...\noindent\includegraphics{cc_by_4-0.eps} | |
| ? | |
| ! Emergency stop. | |
| ... | |
| l.1861 ...\noindent\includegraphics{cc_by_4-0.eps} | |
| ! ==> Fatal error occurred, no output PDF file produced! | |
| Transcript written on main.log. | |
| [verbose]: pdflatex 'main.tex' failed. | |
| [verbose]: Removing (La)TeX AUX file called 'main.aux' (1582460899 >= 1582460896) | |
| [verbose]: Removing (La)TeX AUX file called 'main.out' (1582460899 >= 1582460896) | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running pdflatex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && pdflatex 'main.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex) | |
| restricted \write18 enabled. | |
| entering extended mode | |
| (./main.tex | |
| LaTeX2e <2016/03/31> patch level 3 | |
| Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. | |
| (./texdirectives.tex) (./llncs.cls | |
| Document Class: llncs 2018/03/10 v2.20 | |
| LaTeX document class for Lecture Notes in Computer Science | |
| (/texlive/2016/texmf-dist/tex/latex/base/article.cls | |
| Document Class: article 2014/09/29 v1.4h Standard LaTeX document class | |
| (/texlive/2016/texmf-dist/tex/latex/base/size10.clo)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty | |
| (/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/times.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/dejavu/DejaVuSansMono.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/scalerel/scalerel.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tools/calc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-def/pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) | |
| (/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/wrapfig/wrapfig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/titlesec/titlesec.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/booktabs/booktabs.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/subcaption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption3.sty) | |
| Package caption Warning: Unsupported document class (or package) detected, | |
| (caption) usage of the caption package is not recommended. | |
| See the caption package documentation for explanation. | |
| )) (/texlive/2016/texmf-dist/tex/latex/semantic/semantic.sty | |
| Semantic Package v2.0(epsilon) [2003/10/28] | |
| CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ | |
| Loading features: | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, | |
| and general definitions. | |
| ) (/texlive/2016/texmf-dist/tex/latex/amsmath/amsmath.sty | |
| For additional information on amsmath, use the `?' option. | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amstext.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsgen.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsbsy.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsopn.sty) | |
| Package amsmath Warning: Unable to redefine math accent \vec. | |
| ) (/texlive/2016/texmf-dist/tex/latex/mathpartir/mathpartir.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/xspace.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/latexsym.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mathtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mhsetup.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/color.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.sty | |
| (/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/verbatim.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def | |
| (/texlive/2016/texmf-dist/tex/latex/ms/everyshi.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/dvipsnam.def)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.c | |
| ode.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex | |
| ) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmet | |
| ics.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code. | |
| tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.cod | |
| e.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex)) | |
| ) (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty | |
| )) (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgffor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/math/pgfmath.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arytopaths.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypositioning.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshadows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfadings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex) | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryarrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arycalc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arybackgrounds.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfit.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.geometric.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geo | |
| metric.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.misc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mis | |
| c.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.symbols.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.sym | |
| bols.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.arrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arr | |
| ows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.callouts.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.cal | |
| louts.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.multipart.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mul | |
| tipart.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.pathreplacing.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.pathreplacing.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypatterns.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.markings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.markings.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikzscale/tikzscale.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3packages/xparse/xparse.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3-code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/letltxmacro.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.tex))) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/t1enc.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/bera/beramono.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/epigraph/epigraph.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/float/float.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/refcount.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/gettitlestring.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/kvoptions.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/kvsetkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/etexcmds.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty)))))) | |
| (/texlive/2016/texmf-dist/tex/latex/changepage/changepage.sty) (./coqed.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/bm.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/cancel/cancel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/centernot.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-restate.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thmtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-patch.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/parseargs.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-kv.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-autoref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/aliasctr.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-listof.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-llncs.sty | |
| Package thmtools Warning: LLNCS support disables automatic casing of theorem na | |
| mes . | |
| ))) (/texlive/2016/texmf-dist/tex/latex/enumitem/enumitem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fancyvrb/fancyvrb.sty | |
| Style option: `fancyvrb' v2.7a, with DG/SPQR fixes, and firstline=lastline fix | |
| <2008/02/07> (tvz)) (/texlive/2016/texmf-dist/tex/latex/varwidth/varwidth.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/combelow/combelow.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/bussproofs/bussproofs.sty | |
| Proof Tree (bussproofs) style macros. Version 1.1. | |
| ) (/texlive/2016/texmf-dist/tex/generic/ulem/ulem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/yhmath/yhmath.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xy.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes, | |
| docmode, (/texlive/2016/texmf-dist/tex/generic/xypic/xyrecat.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyidioms.tex) | |
| Xy-pic version 3.8.9 <2013/10/06> | |
| Copyright (c) 1991-2013 by Kristoffer H. Rose <krisrose@tug.org> and others | |
| Xy-pic is free software: see the User's Guide for details. | |
| Loading kernel: messages; fonts; allocations: state, direction, | |
| utility macros; pictures: \xy, positions, objects, decorations; | |
| kernel objects: directionals, circles, text; options; algorithms: directions, | |
| edges, connections; Xy-pic loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/ifpdf.sty) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyall.tex | |
| Xy-pic option: All features v.3.8 | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycurve.tex | |
| Xy-pic option: Curve and Spline extension v.3.12 curve, circles, loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyframe.tex | |
| Xy-pic option: Frame and Bracket extension v.3.14 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycmtip.tex | |
| Xy-pic option: Computer Modern tip extension v.3.7 | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xytips.tex | |
| Xy-pic option: More Tips extension v.3.11 loaded) loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyline.tex | |
| Xy-pic option: Line styles extension v.3.10 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyrotate.tex | |
| Xy-pic option: Rotate and Scale extension v.3.8 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xycolor.tex | |
| Xy-pic option: Colour extension v.3.11 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xymatrix.tex | |
| Xy-pic option: Matrix feature v.3.14 loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xyarrow.tex | |
| Xy-pic option: Arrow and Path feature v.3.9 path, \ar, loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xygraph.tex | |
| Xy-pic option: Graph feature v.3.11 loaded) loaded) | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf.tex | |
| Xy-pic option: PDF driver v.1.7 Xy-pic pdf driver: `color' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-co.tex loaded) | |
| Xy-pic pdf driver: `curve' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-cu.tex loaded) | |
| Xy-pic pdf driver: `frame' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-fr.tex loaded) | |
| Xy-pic pdf driver: `line' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-li.tex loaded) | |
| Xy-pic pdf driver: `rotate' extension support | |
| (/texlive/2016/texmf-dist/tex/generic/xypic/xypdf-ro.tex loaded) loaded)) | |
| (/texlive/2016/texmf-local/tex/latex/natbib/natbib.sty | |
| This is natbib version 8.31 | |
| ************************************************************* | |
| !!WARNING!! !!WARNING!! !!WARNING!! !!WARNING!! | |
| This version (v8.31) of natbib is stricter in its formatting | |
| requirements for bibitem entries than the previous version | |
| used at arXiv (v7.1). | |
| If your submission encounters a problem see | |
| http://arXiv.org/help/faq/texlive | |
| and the natbib documentation at | |
| http://www.ctan.org/tex-archive/macros/latex/contrib/natbib/ | |
| for explanation and adjust your submission accordingly. | |
| The arXiv team. | |
| ************************************************************* | |
| ) (/texlive/2016/texmf-dist/tex/latex/hyperref/hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/auxhook.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/pd1enc.def) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/hyperref.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/url/url.sty)) | |
| Package hyperref Message: Driver: hpdftex. | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/hpdftex.def | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/cleveref/cleveref.sty) (./cmds.tex) | |
| No file main.aux. | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/t1ptm.fd) | |
| (/texlive/2016/texmf-dist/tex/context/base/mkii/supp-pdf.mkii | |
| [Loading MPS to PDF converter (version 2006.09.02).] | |
| ) (/texlive/2016/texmf-dist/tex/latex/oberdiek/epstopdf-base.sty | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/grfext.sty) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/epstopdf-sys.cfg)) | |
| ABD: EveryShipout initializing macros | |
| (/texlive/2016/texmf-dist/tex/latex/yhmath/OMXyhex.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ulasy.fd) | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\\' on input line 523. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 523. | |
| (./abstract.tex) (./intro.tex | |
| Package natbib Warning: Citation `McCarthyP67' on page 1 undefined on input lin | |
| e 13. | |
| Package natbib Warning: Citation `MilnerW72' on page 1 undefined on input line | |
| 13. | |
| Package natbib Warning: Citation `Morris73a' on page 1 undefined on input line | |
| 13. | |
| Package natbib Warning: Citation `Leroy09' on page 1 undefined on input line 17 | |
| . | |
| Package natbib Warning: Citation `SevcikVNJS13' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `MullenZTG16' on page 1 undefined on input lin | |
| e 20. | |
| Package natbib Warning: Citation `StewartBCA15' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `KangKHDV15' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `KangHMGZV15' on page 1 undefined on input lin | |
| e 20. | |
| Package natbib Warning: Citation `BessonBW19' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `WangWS19' on page 1 undefined on input line 2 | |
| 0. | |
| Package natbib Warning: Citation `GuSKWKS0CR18' on page 1 undefined on input li | |
| ne 20. | |
| Package natbib Warning: Citation `RamananandroSWKF15' on page 1 undefined on in | |
| put line 20. | |
| Package natbib Warning: Citation `CarbonneauxHRS14' on page 1 undefined on inpu | |
| t line 20. | |
| Package natbib Warning: Citation `BoldoJLM15' on page 1 undefined on input line | |
| 20. | |
| Package natbib Warning: Citation `ZhaoNMZ12' on page 1 undefined on input line | |
| 23. | |
| Package natbib Warning: Citation `NeisHKMDV15' on page 1 undefined on input lin | |
| e 24. | |
| Package natbib Warning: Citation `TanMKFON19' on page 1 undefined on input line | |
| 25. | |
| Package natbib Warning: Citation `CertiCoq17' on page 1 undefined on input line | |
| 27. | |
| Package natbib Warning: Citation `SecureCompilationSIGPLAN19' on page 1 undefin | |
| ed on input line 48. | |
| Package natbib Warning: Citation `dagstuhl-sc-2018' on page 1 undefined on inpu | |
| t line 48. | |
| Package natbib Warning: Citation `Leroy09' on page 1 undefined on input line 66 | |
| . | |
| Package natbib Warning: Citation `TanMKFON19' on page 1 undefined on input line | |
| 67. | |
| [1{/texlive/2016/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 78 | |
| . | |
| LaTeX Warning: Reference `sec:secure-compilation' on page 2 undefined on input | |
| line 142. | |
| Package natbib Warning: Citation `patrignani2020use' on page 2 undefined on inp | |
| ut line 152. | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 18 | |
| 2. | |
| Package natbib Warning: Citation `Leroy09' on page 2 undefined on input line 18 | |
| 4. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 1 | |
| 87. | |
| Package natbib Warning: Citation `Heartbleed' on page 2 undefined on input line | |
| 201. | |
| Package natbib Warning: Citation `memory-unsafety' on page 2 undefined on input | |
| line 201. | |
| Package natbib Warning: Citation `HallerJPPGBK16' on page 2 undefined on input | |
| line 201. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 02. | |
| Package natbib Warning: Citation `Lattner11' on page 2 undefined on input line | |
| 202. | |
| Package natbib Warning: Citation `WangZKS13' on page 2 undefined on input line | |
| 202. | |
| Package natbib Warning: Citation `WangCCJZK12' on page 2 undefined on input lin | |
| e 202. | |
| (/texlive/2016/texmf-dist/tex/latex/bera/t1fvm.fd) | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 08. | |
| Package natbib Warning: Citation `Regehr10' on page 2 undefined on input line 2 | |
| 12. | |
| Package natbib Warning: Citation `TanMKFON19' on page 2 undefined on input line | |
| 218. | |
| [2] | |
| LaTeX Warning: Reference `def:bcc' on page 3 undefined on input line 268. | |
| [3] | |
| Package natbib Warning: Citation `LamportS84' on page 4 undefined on input line | |
| 432. | |
| LaTeX Font Warning: Font shape `U/stmry/b/n' undefined | |
| (Font) using `U/stmry/m/n' instead on input line 440. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 4 undefined on | |
| input line 511. | |
| Package natbib Warning: Citation `backhouse2004safety' on page 4 undefined on i | |
| nput line 511. | |
| Package natbib Warning: Citation `naumann1998categorical' on page 4 undefined o | |
| n input line 511. | |
| LaTeX Warning: Reference `fig:diagram-cc' on page 4 undefined on input line 571 | |
| . | |
| (./diagram-cc-only.tex) [4] | |
| LaTeX Warning: Reference `sec:trinity' on page 5 undefined on input line 628. | |
| LaTeX Warning: Reference `fig:diagram-cc' on page 5 undefined on input line 629 | |
| . | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 5 undefined on | |
| input line 641. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 5 undefined on input line | |
| 643. | |
| LaTeX Warning: Reference `sec:example-undef' on page 5 undefined on input line | |
| 732. | |
| LaTeX Warning: Reference `sec:example-resources' on page 5 undefined on input l | |
| ine 733. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 5 undefined on input | |
| line 734. | |
| LaTeX Warning: Reference `sec:example-split-io' on page 5 undefined on input li | |
| ne 736. | |
| Package natbib Warning: Citation `GoguenM82' on page 5 undefined on input line | |
| 758. | |
| LaTeX Warning: Reference `sec:example-noninterference' on page 5 undefined on i | |
| nput line 761. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 5 undefined o | |
| n input line 764. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 5 undefined on input li | |
| ne 799. | |
| LaTeX Warning: Reference `sec:secure-compilation' on page 5 undefined on input | |
| line 801. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 5 undefined on input li | |
| ne 811. | |
| LaTeX Warning: Reference `sec:related' on page 5 undefined on input line 823. | |
| LaTeX Warning: Reference `sec:conclusion' on page 5 undefined on input line 823 | |
| . | |
| <coq.pdf, id=93, 449.06996pt x 553.30359pt> <use coq.pdf>) | |
| LaTeX Warning: Reference `sec:correct-trace-props' on page 5 undefined on input | |
| line 637. | |
| LaTeX Warning: Reference `thm:galois' on page 5 undefined on input line 641. | |
| LaTeX Warning: Reference `sec:trinity' on page 5 undefined on input line 671. | |
| Package natbib Warning: Citation `ClarksonS10' on page 5 undefined on input lin | |
| e 681. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 5 undefined on input line | |
| 686. | |
| Underfull \vbox (badness 5105) has occurred while \output is active [5 <./coq.p | |
| df>] | |
| LaTeX Warning: Reference `sec:intro' on page 6 undefined on input line 738. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.1} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.757 \begin{definition} | |
| [\tpsigma and \tptau] \label{defn:TP} | |
| Package natbib Warning: Citation `CousotCousot77-1' on page 6 undefined on inpu | |
| t line 797. | |
| Package natbib Warning: Citation `Melton:1986' on page 6 undefined on input lin | |
| e 797. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.2} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.799 \begin{definition} | |
| [Galois connection] Let $(X, \preceq)$ and | |
| Overfull \hbox (4.70688pt too wide) in paragraph at lines 818--821 | |
| []\T1/ptm/b/n/10 (Characteristic prop-erty of Ga-lois con-nec-tions). [][]\T1/p | |
| tm/m/it/10 If $\OML/cmm/m/it/10 []\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 X; \OMS/cm | |
| sy/m/n/10 ^^V\OT1/cmr/m/n/10 ) \U/msa/m/n/10 ^^\ []$ | |
| [6] | |
| LaTeX Warning: Reference `lem:chG' on page 7 undefined on input line 835. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `lem:correspond' on page 7 undefined on input line 871 | |
| . | |
| LaTeX Warning: Reference `thm:correspondcriteria' on page 7 undefined on input | |
| line 872. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 7 undefined on input l | |
| ine 882. | |
| Package natbib Warning: Citation `TanMKFON19' on page 7 undefined on input line | |
| 882. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 7 undefined on | |
| input line 884. | |
| LaTeX Warning: Reference `defn:TP' on page 7 undefined on input line 897. | |
| LaTeX Warning: Reference `sec:intro' on page 7 undefined on input line 898. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:galois' on page 7 undefined on input line 907. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:correspondcriteria' on page 7 undefined on input | |
| line 910. | |
| Package natbib Warning: Citation `gardiner1994algebraic' on page 7 undefined on | |
| input line 942. | |
| <use coq.pdf> [7] | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 999. | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 1012. | |
| LaTeX Warning: Reference `lem:correspond' on page 8 undefined on input line 101 | |
| 5. | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 8 undefined on input lin | |
| e 1017. | |
| LaTeX Warning: Reference `sec:example-resources' on page 8 undefined on input l | |
| ine 1046. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1111. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1114. | |
| LaTeX Warning: Reference `thm:ssch' on page 8 undefined on input line 1121. | |
| Package natbib Warning: Citation `ClarksonS10' on page 8 undefined on input lin | |
| e 1128. | |
| LaTeX Warning: Reference `sec:trinity' on page 8 undefined on input line 1155. | |
| [8] | |
| Package natbib Warning: Citation `mastroeni2018verifying' on page 9 undefined o | |
| n input line 1176. | |
| Package natbib Warning: Citation `naumann2019whither' on page 9 undefined on in | |
| put line 1176. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:ssch' on page 9 undefined on input line 1204. | |
| LaTeX Warning: Reference `sec:example-noninterference' on page 9 undefined on i | |
| nput line 1207. | |
| LaTeX Warning: Reference `sec:example-undef' on page 9 undefined on input line | |
| 1223. | |
| LaTeX Warning: Reference `sec:example-resources' on page 9 undefined on input l | |
| ine 1227. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 9 undefined on input | |
| line 1229. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 9 undefined on input line | |
| 1232. | |
| (./undefbeh.tex | |
| LaTeX Warning: Reference `sec:intro' on page 9 undefined on input line 3. | |
| LaTeX Warning: Reference `sec:intro' on page 9 undefined on input line 49. | |
| <use coq.pdf> [9] | |
| Package natbib Warning: Citation `CaoBGDA18' on page 10 undefined on input line | |
| 165. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 10 undefined on input li | |
| ne 182. | |
| ) (./resource-exhaustion.tex | |
| LaTeX Warning: Reference `sec:intro' on page 10 undefined on input line 4. | |
| <use coq.pdf> [10] | |
| Package natbib Warning: Citation `LamportS84' on page 11 undefined on input lin | |
| e 107. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `sec:safety-preservation' on page 11 undefined on inpu | |
| t line 115. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 11 undefined on inpu | |
| t line 153. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `DeepSpecLeroy' on page 11 undefined on input | |
| line 171. | |
| ) (./diff_values.tex <use coq.pdf> [11] | |
| LaTeX Warning: Reference `tr:ste-con' on page 1 undefined on input line 127. | |
| LaTeX Warning: Reference `tr:ste-em' on page 1 undefined on input line 127. | |
| LaTeX Warning: Reference `tr:ste-b' on page 1 undefined on input line 128. | |
| LaTeX Warning: Reference `tr:ste-n' on page 1 undefined on input line 128. | |
| (/texlive/2016/texmf-dist/tex/latex/psnfss/t1phv.fd) <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-dv-cc' on page 12 undefined on input line 20 | |
| 9. | |
| Package natbib Warning: Citation `Engelfriet85' on page 12 undefined on input l | |
| ine 214. | |
| Package natbib Warning: Citation `milner82' on page 12 undefined on input line | |
| 214. | |
| Package natbib Warning: Citation `ZakinthinosL97' on page 12 undefined on input | |
| line 215. | |
| Package natbib Warning: Citation `FocardiG95' on page 12 undefined on input lin | |
| e 215. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 12 undefined on input | |
| line 218. | |
| Package natbib Warning: Citation `Leroy09b' on page 12 undefined on input line | |
| 218. | |
| Package natbib Warning: Citation `BeringerSDA14' on page 12 undefined on input | |
| line 225. | |
| Package natbib Warning: Citation `Leroy09b' on page 12 undefined on input line | |
| 225. | |
| <xymatrix 5x3 458> [12] <xymatrix 5x2 386> <use coq.pdf> | |
| Package natbib Warning: Citation `BeringerSDA14' on page 13 undefined on input | |
| line 320. | |
| Package natbib Warning: Citation `Leroy09b' on page 13 undefined on input line | |
| 320. | |
| ) (./instance-more-target-statements.tex | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 13 undefined on inpu | |
| t line 14. | |
| [13] | |
| LaTeX Warning: Reference `tr:tr-rel-n' on page 1 undefined on input line 113. | |
| LaTeX Warning: Reference `tr:tr-rel-m-m' on page 1 undefined on input line 115. | |
| LaTeX Warning: Reference `tr:tr-rel-m-n' on page 1 undefined on input line 115. | |
| LaTeX Warning: Reference `tr:tr-rel-n-m' on page 1 undefined on input line 115. | |
| Underfull \hbox (badness 10000) in paragraph at lines 112--140 | |
| \T1/ptm/m/n/10 build on these rules to de-fine the | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 14 undefined on input line | |
| 142. | |
| LaTeX Warning: Reference `tr:tr-rel-full' on page 1 undefined on input line 149 | |
| . | |
| ) (./ANI.tex | |
| Package natbib Warning: Citation `GoguenM82' on page 14 undefined on input line | |
| 16. | |
| LaTeX Warning: Reference `sec:subset-closed' on page 14 undefined on input line | |
| 17. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 14 undefined | |
| on input line 52. | |
| [14] | |
| LaTeX Warning: Reference `thm:ssch' on page 15 undefined on input line 239. | |
| [15] | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 267. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 386. | |
| Package natbib Warning: Citation `CousotCousot77-1' on page 16 undefined on inp | |
| ut line 388. | |
| Package natbib Warning: Citation `sabelfeld05:_dimensions_declass' on page 16 u | |
| ndefined on input line 392. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 16 undefined | |
| on input line 447. | |
| [16] | |
| LaTeX Warning: Reference `thm:compilingANI' on page 17 undefined on input line | |
| 618. | |
| LaTeX Warning: Reference `sec:trinity' on page 17 undefined on input line 673. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 58. | |
| LaTeX Warning: Reference `sec:instances' on page 17 undefined on input line 759 | |
| . | |
| LaTeX Warning: Reference `sec:example-undef' on page 17 undefined on input line | |
| 760. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 85. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 1 undefined on input line 7 | |
| 94. | |
| [17] | |
| LaTeX Warning: Reference `thm:genANI' on page 1 undefined on input line 842. | |
| Package natbib Warning: Citation `giacobazzi2018abstract' on page 18 undefined | |
| on input line 844. | |
| Package natbib Warning: Citation `AbadiCCD' on page 18 undefined on input line | |
| 874. | |
| Package natbib Warning: Citation `mastroeni2018verifying' on page 18 undefined | |
| on input line 874. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 18 undefined on input lin | |
| e 883. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 18 undefined on input lin | |
| e 885. | |
| Overfull \hbox (15.32541pt too wide) in paragraph at lines 922--927 | |
| []\T1/ptm/b/n/10 (Target ANI by source ANI). [][]\T1/ptm/m/it/10 Let $[][] \OMS | |
| /cmsy/m/n/10 2 []\OT1/cmr/m/n/10 (2[])$\T1/ptm/m/it/10 , $[][] \OMS/cmsy/m/n/10 | |
| 2 []\OT1/cmr/m/n/10 (2[])$ | |
| Package natbib Warning: Citation `BartheGL18' on page 18 undefined on input lin | |
| e 1045. | |
| Package natbib Warning: Citation `DSilvaPS15' on page 18 undefined on input lin | |
| e 1045. | |
| ) (./secure-compilation-motivation.tex [18] | |
| Package natbib Warning: Citation `Leroy09' on page 19 undefined on input line 2 | |
| 8. | |
| Package natbib Warning: Citation `NeisHKMDV15' on page 19 undefined on input li | |
| ne 33. | |
| Package natbib Warning: Citation `StewartBCA15' on page 19 undefined on input l | |
| ine 33. | |
| Package natbib Warning: Citation `HurD11' on page 19 undefined on input line 33 | |
| . | |
| Package natbib Warning: Citation `KangKHDV15' on page 19 undefined on input lin | |
| e 33. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 39. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 96. | |
| LaTeX Warning: Reference `sec:compiler-correctness' on page 19 undefined on inp | |
| ut line 107. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 113. | |
| LaTeX Warning: Reference `sec:sec-comp-trini' on page 19 undefined on input lin | |
| e 117. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 19 undefined on input li | |
| ne 125. | |
| LaTeX Warning: Reference `sec:comp-summ' on page 19 undefined on input line 126 | |
| . | |
| ) (./sec-comp-explain.tex | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 19 undefined on input l | |
| ine 10. | |
| LaTeX Warning: Reference `sec:compiler-correctness' on page 19 undefined on inp | |
| ut line 11. | |
| LaTeX Warning: Reference `thm:rtc-trinity' on page 1 undefined on input line 20 | |
| . | |
| [19] <use coq.pdf>) (./expand-sec-diagram.tex | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 20 undefined on input l | |
| ine 2. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 20 undefined on input l | |
| ine 37. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 20 undefined | |
| on input line 42. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `ClarksonS10' on page 20 undefined on input li | |
| ne 91. | |
| LaTeX Warning: Reference `thm:ssch' on page 20 undefined on input line 94. | |
| [20] <use coq.pdf> <use coq.pdf> | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 21 undefined | |
| on input line 119. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 21 undefined | |
| on input line 173. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 1 undefined o | |
| n input line 213. | |
| (./diagram-prop-pres-comp-security.tex <use coq.pdf> <use coq.pdf> | |
| <use coq.pdf> <use coq.pdf> <use coq.pdf> <use coq.pdf> <use coq.pdf> | |
| <use coq.pdf> <use coq.pdf>)) (./robust-trace.tex [21] | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 22 undefined on inpu | |
| t line 19. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 22 undefined on inpu | |
| t line 145. | |
| Underfull \vbox (badness 2443) has occurred while \output is active [22] | |
| <use coq.pdf>) (./rw-sec-crits-short.tex | |
| Package natbib Warning: Citation `PatrignaniG18' on page 23 undefined on input | |
| line 6. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 23 undefined on inpu | |
| t line 7. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 23 undefined on input | |
| line 19. | |
| ) [23] | |
| Package natbib Warning: Citation `Leroy09' on page 24 undefined on input line 1 | |
| 352. | |
| Package natbib Warning: Citation `TanMKFON19' on page 24 undefined on input lin | |
| e 1352. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 24 undefined on input l | |
| ine 1353. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 24 undefined on input | |
| line 1353. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 24 undefined on input | |
| line 1353. | |
| LaTeX Warning: Reference `thm:rsp-sec-trinity' on page 24 undefined on input li | |
| ne 1359. | |
| Package natbib Warning: Citation `ClarksonS10' on page 24 undefined on input li | |
| ne 1362. | |
| Package natbib Warning: Citation `PasquaM17' on page 24 undefined on input line | |
| 1364. | |
| Package natbib Warning: Citation `XiaZHHMPZ20' on page 24 undefined on input li | |
| ne 1369. | |
| Package natbib Warning: Citation `XiaZHHMPZ20' on page 24 undefined on input li | |
| ne 1371. | |
| Package natbib Warning: Citation `WangWS19' on page 24 undefined on input line | |
| 1402. | |
| LaTeX Warning: Reference `sec:example-undef' on page 24 undefined on input line | |
| 1404. | |
| Package natbib Warning: Citation `SevcikVNJS13' on page 24 undefined on input l | |
| ine 1407. | |
| Package natbib Warning: Citation `KangHMGZV15' on page 24 undefined on input li | |
| ne 1407. | |
| Package natbib Warning: Citation `CarbonneauxHRS14' on page 24 undefined on inp | |
| ut line 1407. | |
| Package natbib Warning: Citation `MullenZTG16' on page 24 undefined on input li | |
| ne 1407. | |
| Package natbib Warning: Citation `TanMKFON19' on page 24 undefined on input lin | |
| e 1407. | |
| LaTeX Warning: Reference `sec:example-resources' on page 24 undefined on input | |
| line 1409. | |
| Package natbib Warning: Citation `HurD11' on page 24 undefined on input line 14 | |
| 57. | |
| Package natbib Warning: Citation `JeffreyR05' on page 24 undefined on input lin | |
| e 1470. | |
| Package natbib Warning: Citation `PatrignaniC15' on page 24 undefined on input | |
| line 1470. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 24 undefined on input l | |
| ine 1470. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 24 undefined | |
| on input line 1474. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1503. | |
| LaTeX Warning: Reference `fig:morris' on page 24 undefined on input line 1506. | |
| Package natbib Warning: Citation `PattersonA19' on page 24 undefined on input l | |
| ine 1509. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1512. | |
| Overfull \hbox (19.37321pt too wide) in paragraph at lines 1535--1536 | |
| [][] | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1557. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1557. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1557. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1557. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1557. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1557. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1557. | |
| Package natbib Warning: Citation `Morris73a' on page 24 undefined on input line | |
| 1557. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1557. | |
| Package natbib Warning: Citation `Melton:1986' on page 24 undefined on input li | |
| ne 1557. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1557. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 24 undefined on | |
| input line 1557. | |
| [24] | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1564. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1564. | |
| LaTeX Warning: Reference `fig:morris' on page 25 undefined on input line 1565. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1566. | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1566. | |
| Package natbib Warning: Citation `cousot2002constructive' on page 25 undefined | |
| on input line 1580. | |
| Package natbib Warning: Citation `Melton:1986' on page 25 undefined on input li | |
| ne 1581. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 25 undefined on | |
| input line 1581. | |
| LaTeX Warning: Reference `sec:relatedwork' on page 25 undefined on input line 1 | |
| 582. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 25 undefined on input l | |
| ine 1604. | |
| Package natbib Warning: Citation `BusiDG19' on page 25 undefined on input line | |
| 1604. | |
| LaTeX Warning: Reference `sec:intro' on page 25 undefined on input line 1678. | |
| (./appendixintro.tex [25] | |
| LaTeX Warning: Reference `sec:pi' on page 1 undefined on input line 5. | |
| LaTeX Warning: Reference `sec:other-classes' on page 1 undefined on input line | |
| 9. | |
| Package natbib Warning: Citation `Melton:1986' on page 26 undefined on input li | |
| ne 11. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 26 undefined on | |
| input line 12. | |
| LaTeX Warning: Reference `sec:relatedwork' on page 1 undefined on input line 12 | |
| . | |
| LaTeX Warning: Reference `sec:instances' on page 1 undefined on input line 14. | |
| LaTeX Warning: Reference `sec:elided' on page 1 undefined on input line 15. | |
| LaTeX Warning: Reference `sec:composition' on page 1 undefined on input line 18 | |
| . | |
| LaTeX Warning: Reference `sec:in-depth-trsec' on page 1 undefined on input line | |
| 21. | |
| ) (./proofindex.tex | |
| LaTeX Warning: Reference `thm:galois' on page 26 undefined on input line 5. | |
| <use coq.pdf> | |
| Overfull \hbox (0.30478pt too wide) in paragraph at lines 5--17 | |
| \T1/ptm/m/n/10 ($\OMS/cmsy/m/n/10 ($\T1/ptm/m/n/10 ) As-sume $[]$ and that $[]$ | |
| sat-is-fies $[] \OMS/cmsy/m/n/10 ^^R \OML/cmm/m/it/10 ^^[\OT1/cmr/m/n/10 (\OML | |
| /cmm/m/it/10 ^^\\OT1/cmr/m/n/10 ([]))$\T1/ptm/m/n/10 . Ap-ply $[]$ to $[]$ and | |
| $\OML/cmm/m/it/10 ^^[\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 ^^\\OT1/cmr/m/n/10 ([])) | |
| $ | |
| LaTeX Warning: Reference `thm:trinitarianview' on page 26 undefined on input li | |
| ne 24. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:galois' on page 26 undefined on input line 27. | |
| Overfull \hbox (2.1672pt too wide) in paragraph at lines 24--28 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 See The-o-rems rel_TC_$\OML/cmm | |
| /m/it/10 ^^\$\T1/ptm/m/n/10 TP and rel_TC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 | |
| TP in \T1/fvm/m/n/10 TraceCriterion.v | |
| LaTeX Warning: Reference `lem:surj_rel' on page 26 undefined on input line 44. | |
| LaTeX Warning: Reference `thm:ssch' on page 26 undefined on input line 109. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-dv-cc' on page 26 undefined on input line 11 | |
| 6. | |
| <use coq.pdf> | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 26 undefined on input line | |
| 121. | |
| LaTeX Warning: Reference `sec:proofs-marco' on page 26 undefined on input line | |
| 122. | |
| LaTeX Warning: Reference `thm:compilingANI' on page 26 undefined on input line | |
| 126. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 138. | |
| [26] | |
| LaTeX Warning: Reference `thm:genANI' on page 27 undefined on input line 197. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 211. | |
| Underfull \hbox (badness 10000) in paragraph at lines 197--216 | |
| [27] | |
| Underfull \hbox (badness 10000) in paragraph at lines 227--230 | |
| LaTeX Warning: Reference `thm:srcANI' on page 28 undefined on input line 238. | |
| LaTeX Warning: Reference `lem:surj_rel' on page 1 undefined on input line 251. | |
| Underfull \hbox (badness 10000) in paragraph at lines 238--256 | |
| LaTeX Warning: Reference `thm:rtc-trinity' on page 28 undefined on input line 2 | |
| 78. | |
| <use coq.pdf> | |
| Overfull \hbox (42.58676pt too wide) in paragraph at lines 278--280 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems rel_RTC_$\OML/cmm/m/ | |
| it/10 ^^\$\T1/ptm/m/n/10 RTP and rel_RTC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 R | |
| TP in \T1/fvm/m/n/10 RobustTraceCriterion.v\T1/ptm/m/n/10 . | |
| LaTeX Warning: Reference `thm:rsp-sec-trinity' on page 28 undefined on input li | |
| ne 283. | |
| <use coq.pdf> | |
| Overfull \hbox (76.64267pt too wide) in paragraph at lines 283--285 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems tilde_RSC_$\OML/cmm/ | |
| m/it/10 ^^[$\T1/ptm/m/n/10 RSP and tilde_RSC_Cl_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m | |
| /n/10 RTP in \T1/fvm/m/n/10 RobustSafetyCriterion.v\T1/ptm/m/n/10 . | |
| LaTeX Warning: Reference `thm:rhp-sec-trinity' on page 28 undefined on input li | |
| ne 288. | |
| <use coq.pdf> | |
| Overfull \hbox (42.74326pt too wide) in paragraph at lines 288--290 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 Lem-mas $\OML/cmm/m/it/10 ^^[$\ | |
| T1/ptm/m/n/10 RHP_rel_RHC and rel_RHC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 RHP | |
| and The-o-rem rel_RHC_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m/n/10 RHP | |
| LaTeX Warning: Reference `thm:rob' on page 28 undefined on input line 293. | |
| <use coq.pdf> | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 28 undefined on input l | |
| ine 302. | |
| Package natbib Warning: Citation `MarcosSurvey' on page 28 undefined on input l | |
| ine 302. | |
| Package natbib Warning: Citation `Ahmed:2016:ICFP:UnivEmb' on page 28 undefined | |
| on input line 302. | |
| Package natbib Warning: Citation `skorstengaard-stktokens:2019' on page 28 unde | |
| fined on input line 302. | |
| LaTeX Warning: Reference `thm:trini-safe' on page 28 undefined on input line 33 | |
| 6. | |
| <use coq.pdf> | |
| Overfull \hbox (20.5833pt too wide) in paragraph at lines 336--339 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems tilde_SC_$\OML/cmm/m | |
| /it/10 ^^[$\T1/ptm/m/n/10 SP and tilde_SC_Cl_$\OML/cmm/m/it/10 ^^\$\T1/ptm/m/n/ | |
| 10 TP in \T1/fvm/m/n/10 SafetyCriterion.v\T1/ptm/m/n/10 . | |
| [28] | |
| LaTeX Warning: Reference `thm:eq-hp' on page 29 undefined on input line 343. | |
| LaTeX Warning: Reference `thm:wktr' on page 29 undefined on input line 353. | |
| <use coq.pdf> | |
| Overfull \hbox (49.34982pt too wide) in paragraph at lines 353--355 | |
| []\T1/ptm/m/it/10 (Of [] ([])). \T1/ptm/m/n/10 The-o-rems rel_HC_$\OML/cmm/m/i | |
| t/10 ^^\$\T1/ptm/m/n/10 HP, rel_HC_$\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 HP and | |
| $\OML/cmm/m/it/10 ^^[$\T1/ptm/m/n/10 HP_rel_HC in \T1/fvm/m/n/10 HyperCriterion | |
| .v\T1/ptm/m/n/10 . | |
| ) (./appendix-other.tex | |
| LaTeX Warning: Reference `sec:safety-preservation' on page 29 undefined on inpu | |
| t line 15. | |
| LaTeX Warning: Reference `sec:correct-hyper' on page 29 undefined on input line | |
| 17. | |
| Package natbib Warning: Citation `ClarksonS10' on page 29 undefined on input li | |
| ne 43. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.1} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.56 \begin{definition} | |
| [Safety Properties] | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 29 undefined on input l | |
| ine 90. | |
| pdfTeX warning (ext4): destination with the same identifier (name{definition.2} | |
| ) has been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.100 \begin{definition} | |
| [$\sctilde$] | |
| LaTeX Warning: Reference `sec:subset-closed' on page 29 undefined on input line | |
| 114. | |
| [29] | |
| Overfull \hbox (4.73111pt too wide) in paragraph at lines 126--129 | |
| []\T1/ptm/b/n/10 (Trinitarian view for Safety). [][]\T1/ptm/m/it/10 For a trace | |
| re-la-tion $\OMS/cmsy/m/n/10 ^^X ^^R [] ^^B []$ | |
| Overfull \hbox (10.21405pt too wide) in paragraph at lines 136--136 | |
| [] | |
| (./diagram-sc-only.tex) | |
| Overfull \hbox (17.11406pt too wide) in paragraph at lines 130--143 | |
| [] $[]$ $[]$ | |
| Package natbib Warning: Citation `ClarksonS10' on page 30 undefined on input li | |
| ne 179. | |
| (./diagram-hc-only.tex) | |
| Overfull \hbox (16.90001pt too wide) in paragraph at lines 241--255 | |
| []$[]$ $[]$ | |
| [30] | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-cc' on page 31 undefined o | |
| n input line 257. | |
| (./diagram-prop-pres-comp-corr.tex)) (./other_works.tex | |
| Package natbib Warning: Citation `Melton:1986' on page 31 undefined on input li | |
| ne 102. | |
| Package natbib Warning: Citation `sabry1997reflection' on page 31 undefined on | |
| input line 103. | |
| Package natbib Warning: Citation `Melton:1986' on page 31 undefined on input li | |
| ne 104. | |
| ) (./app-proofs-marco-statements.tex | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 1 undefined on input | |
| line 4. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 4. | |
| Overfull \hbox (4.3616pt too wide) in paragraph at lines 35--35 | |
| [] | |
| [31] <use coq.pdf> | |
| LaTeX Warning: Reference `tr:sem-nat' on page 1 undefined on input line 180. | |
| LaTeX Warning: Reference `tr:sem-in-nat' on page 1 undefined on input line 180. | |
| LaTeX Warning: Reference `tr:sem-s-nat' on page 1 undefined on input line 180. | |
| Overfull \hbox (29.37361pt too wide) in paragraph at lines 253--253 | |
| [] | |
| [32] | |
| LaTeX Warning: Reference `SEC:M' on page 1 undefined on input line 259. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 259. | |
| Overfull \hbox (40.73592pt too wide) in paragraph at lines 287--287 | |
| [] | |
| [33] | |
| Overfull \hbox (30.26236pt too wide) in paragraph at lines 550--550 | |
| [] | |
| LaTeX Warning: Reference `SEC:M' on page 1 undefined on input line 573. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 573. | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 1 undefined on input line | |
| 574. | |
| LaTeX Warning: Reference `thm:inst-marco-gensend' on page 1 undefined on input | |
| line 575. | |
| LaTeX Warning: Reference `thm:inst-marco-cc-expr' on page 1 undefined on input | |
| line 576. | |
| pdfTeX warning (ext4): destination with the same identifier (name{lemma.1}) has | |
| been already used, duplicate ignored | |
| <to be read again> | |
| \relax | |
| l.580 \begin{lemma} | |
| [\gensends{\cdot} works]\label{thm:inst-marco-gensend} | |
| Overfull \hbox (58.24623pt too wide) in paragraph at lines 580--587 | |
| []\T1/ptm/b/n/10 ($[]$ works). [][]$[][][][][][] [] []$ | |
| Overfull \hbox (2.40167pt too wide) in paragraph at lines 595--596 | |
| []$[]$ \T1/ptm/m/n/10 trans-lates that into $[]$. | |
| LaTeX Warning: Reference `tr:e-tm-send' on page 1 undefined on input line 597. | |
| [34] | |
| LaTeX Warning: Reference `tr:tr-rel-n' on page 1 undefined on input line 602. | |
| Overfull \hbox (8.17157pt too wide) in paragraph at lines 619--619 | |
| [] | |
| Overfull \hbox (16.16049pt too wide) in paragraph at lines 621--632 | |
| []\T1/ptm/m/n/10 By as-sump-tion we have HP1 $[]$ | |
| LaTeX Warning: Reference `tr:tr-rel-m-m' on page 1 undefined on input line 649. | |
| LaTeX Warning: Reference `tr:tr-rel-n-m' on page 1 undefined on input line 657. | |
| LaTeX Warning: Reference `tr:tr-rel-m-n' on page 1 undefined on input line 661. | |
| Overfull \hbox (19.9337pt too wide) in paragraph at lines 667--673 | |
| []\T1/ptm/b/n/10 ($[][]$ is cor-rect for ex-pres-sions). [][]$[][][][]$ | |
| LaTeX Warning: Reference `thm:inst-marco-cc' on page 35 undefined on input line | |
| 681. | |
| LaTeX Warning: Reference `thm:inst-marco-cc-expr' on page 35 undefined on input | |
| line 697. | |
| LaTeX Warning: Reference `thm:inst-marco-gensend' on page 35 undefined on input | |
| line 703. | |
| LaTeX Warning: Reference `tr:es-sm-send' on page 1 undefined on input line 708. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 1 undefined on input lin | |
| e 718. | |
| Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): | |
| (hyperref) removing `\new@ifnextchar' on input line 718. | |
| Overfull \hbox (10.78104pt too wide) in paragraph at lines 750--750 | |
| [] | |
| ) (./composition-appendix.tex [35] | |
| LaTeX Warning: Reference `sec:trinity' on page 1 undefined on input line 44. | |
| ) | |
| LaTeX Warning: Reference `sec:comp-summ' on page 36 undefined on input line 181 | |
| 9. | |
| (./rob-pres-safety.tex | |
| Package natbib Warning: Citation `patrignani_thesis' on page 36 undefined on in | |
| put line 15. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 36 undefined on input | |
| line 15. | |
| Package natbib Warning: Citation `AbateBGHPT19' on page 36 undefined on input l | |
| ine 15. | |
| Package natbib Warning: Citation `JuglaretHAEP16' on page 36 undefined on input | |
| line 15. | |
| Package natbib Warning: Citation `JeffreyR05' on page 36 undefined on input lin | |
| e 17. | |
| Package natbib Warning: Citation `PatrignaniG18' on page 36 undefined on input | |
| line 22. | |
| LaTeX Warning: Reference `fig:diagram-preserve-props-sec' on page 36 undefined | |
| on input line 24. | |
| LaTeX Warning: Reference `sec:sec-comp-traces' on page 1 undefined on input lin | |
| e 30. | |
| LaTeX Warning: Reference `sec:instance-marco' on page 1 undefined on input line | |
| 30. | |
| LaTeX Warning: Reference `sec:example-diff-values' on page 1 undefined on input | |
| line 30. | |
| Package natbib Warning: Citation `Schneider00' on page 36 undefined on input li | |
| ne 35. | |
| [36] | |
| Package natbib Warning: Citation `MarcosSurvey' on page 37 undefined on input l | |
| ine 51. | |
| Package natbib Warning: Citation `Leroy09b' on page 37 undefined on input line | |
| 51. | |
| ) (./instance-marcodeepak.tex | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 32. | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 41. | |
| Overfull \hbox (15.95178pt too wide) in paragraph at lines 98--98 | |
| [] | |
| Package natbib Warning: Citation `PatrignaniG17' on page 37 undefined on input | |
| line 99. | |
| ) (./main.bbl [37] [38] [39]) | |
| Underfull \hbox (badness 4699) in paragraph at lines 1856--1857 | |
| \T1/ptm/b/n/9 Open Ac-cess \T1/ptm/m/n/9 This chap-ter is li-censed un-der the | |
| terms of the Cre-ative Com-mons | |
| Overfull \hbox (10.0886pt too wide) in paragraph at lines 1856--1857 | |
| \T1/ptm/m/n/9 Attribution 4.0 In-ter-na-tional Li-cense ([][]$\T1/fvm/m/n/9 htt | |
| p : / / creativecommons . org / licenses / by / 4 . 0/$[][]\T1/ptm/m/n/9 ), whi | |
| ch | |
| Underfull \hbox (badness 10000) in paragraph at lines 1858--1859 | |
| \T1/ptm/m/n/9 cluded in the chap-ter's Cre-ative Com-mons li-cense and your in- | |
| tended | |
| ! Package pdftex.def Error: File `cc_by_4-0.pdf' not found. | |
| See the pdftex.def package documentation for explanation. | |
| Type H <return> for immediate help. | |
| ... | |
| l.1860 ...\noindent\includegraphics{cc_by_4-0.eps} | |
| ? | |
| ! Emergency stop. | |
| ... | |
| l.1860 ...\noindent\includegraphics{cc_by_4-0.eps} | |
| ! ==> Fatal error occurred, no output PDF file produced! | |
| Transcript written on main.log. | |
| [verbose]: pdflatex 'main.tex' failed. | |
| [verbose]: Removing (La)TeX AUX file called 'main.aux' (1582460901 >= 1582460899) | |
| [verbose]: Removing (La)TeX AUX file called 'main.out' (1582460901 >= 1582460899) | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'main.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./main.tex | |
| ! Undefined control sequence. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| ? | |
| ! Emergency stop. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| No pages of output. | |
| Transcript written on main.log. | |
| [verbose]: tex 'main.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'main.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./main.tex | |
| ! Undefined control sequence. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| ? | |
| ! Emergency stop. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| No pages of output. | |
| Transcript written on main.log. | |
| [verbose]: tex 'main.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'main.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'prisc.tex' | |
| [verbose]: arXiv Warning: user included plain hyperref directive. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running hpdflatex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && pdflatex 'prisc.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex) | |
| restricted \write18 enabled. | |
| entering extended mode | |
| (./prisc.tex | |
| LaTeX2e <2016/03/31> patch level 3 | |
| Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. | |
| (/texlive/2016/texmf-dist/tex/latex/acmart/acmart.cls | |
| Document Class: acmart 2016/11/16 v1.24 Typesetting articles for Association of | |
| Computing Machinery | |
| (/texlive/2016/texmf-dist/tex/latex/xkeyval/xkeyval.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/xkeyval.tex | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/xkvutils.tex | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/keyval.tex)))) | |
| (/texlive/2016/texmf-dist/tex/latex/amscls/amsart.cls | |
| Document Class: amsart 2015/03/04 v2.20.2 | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsmath.sty | |
| For additional information on amsmath, use the `?' option. | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amstext.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsgen.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsbsy.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsopn.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype.sty | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype-pdftex.def) | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/totpages/totpages.sty | |
| (/texlive/2016/texmf-dist/tex/latex/ms/everyshi.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/environ/environ.sty | |
| (/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty)) | |
| (/texlive/2016/texmf-local/tex/latex/natbib/natbib.sty | |
| This is natbib version 8.31 | |
| ************************************************************* | |
| !!WARNING!! !!WARNING!! !!WARNING!! !!WARNING!! | |
| This version (v8.31) of natbib is stricter in its formatting | |
| requirements for bibitem entries than the previous version | |
| used at arXiv (v7.1). | |
| If your submission encounters a problem see | |
| http://arXiv.org/help/faq/texlive | |
| and the natbib documentation at | |
| http://www.ctan.org/tex-archive/macros/latex/contrib/natbib/ | |
| for explanation and adjust your submission accordingly. | |
| The arXiv team. | |
| ************************************************************* | |
| ) (/texlive/2016/texmf-dist/tex/latex/hyperref/hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/auxhook.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/kvoptions.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/pd1enc.def) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/hyperref.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/url/url.sty)) | |
| Package hyperref Message: Driver (autodetected): hpdftex. | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/hpdftex.def | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-def/pdftex.def))) | |
| (/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/dvipsnam.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/geometry/geometry.sty | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/geometry.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/ncctools/manyfoot.sty | |
| (/texlive/2016/texmf-dist/tex/latex/ncctools/nccfoots.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/libertine.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/mweights/mweights.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fontaxes/fontaxes.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/LinLibertine_I.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/inconsolata/zi4.sty | |
| `inconsolata-zi4' v1.10, 2016/02/22 Text macros for Inconsolata (msharpe)) | |
| (/texlive/2016/texmf-dist/tex/latex/newtx/newtxmath.sty | |
| `newtxmath' v1.514, 2016/11/18 Math macros based on txfonts (msharpe) | |
| (/texlive/2016/texmf-dist/tex/generic/kastrup/binhex.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption3.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/float/float.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/comment/comment.sty | |
| Excluding comment 'comment') Excluding comment 'CCSXML' | |
| (/texlive/2016/texmf-arxiv/tex/latex/fancyhdr/fancyhdr.sty) | |
| Special comment 'acks' Include comment 'screenonly' | |
| Excluding comment 'printonly' Include comment 'anonsuppress' | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/OT1LinuxLibertineT-TLF.fd)) | |
| (/texlive/2016/texmf-dist/tex/latex/booktabs/booktabs.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/subcaption.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/semantic.sty | |
| Semantic Package v2.0(epsilon) [2003/10/28] | |
| CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ | |
| Loading features: | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, | |
| and general definitions. | |
| ) (/texlive/2016/texmf-dist/tex/latex/mathpartir/mathpartir.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/xspace.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/latexsym.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mathtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tools/calc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mhsetup.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.sty | |
| (/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/verbatim.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.c | |
| ode.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex | |
| ) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmet | |
| ics.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code. | |
| tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.cod | |
| e.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex)) | |
| ) (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty | |
| )) (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgffor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/math/pgfmath.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arytopaths.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypositioning.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshadows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfadings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex) | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryarrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arycalc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arybackgrounds.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfit.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.geometric.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geo | |
| metric.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.misc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mis | |
| c.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.symbols.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.sym | |
| bols.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.arrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arr | |
| ows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.callouts.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.cal | |
| louts.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.multipart.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mul | |
| tipart.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.pathreplacing.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.pathreplacing.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypatterns.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.markings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.markings.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikzscale/tikzscale.sty | |
| (/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/l3packages/xparse/xparse.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3-code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.tex))) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/t1enc.def) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/T1LinuxLibertineT-TLF.fd)) | |
| (/texlive/2016/texmf-dist/tex/latex/bera/beramono.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/epigraph/epigraph.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/wrapfig/wrapfig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/scalerel/scalerel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/changepage/changepage.sty) (./coqed.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/bm.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/cancel/cancel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/centernot.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-restate.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thmtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-patch.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/parseargs.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-kv.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-autoref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/aliasctr.sty | |
| (/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-listof.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-amsthm.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/enumitem/enumitem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fancyvrb/fancyvrb.sty | |
| Style option: `fancyvrb' v2.7a, with DG/SPQR fixes, and firstline=lastline fix | |
| <2008/02/07> (tvz)) (/texlive/2016/texmf-dist/tex/latex/varwidth/varwidth.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/combelow/combelow.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/bussproofs/bussproofs.sty | |
| Proof Tree (bussproofs) style macros. Version 1.1. | |
| ) (/texlive/2016/texmf-dist/tex/generic/ulem/ulem.sty) | |
| ! LaTeX Error: Option clash for package hyperref. | |
| See the LaTeX manual or LaTeX Companion for explanation. | |
| Type H <return> for immediate help. | |
| ... | |
| l.207 \usepackage | |
| {hyperref} | |
| ? | |
| ! Emergency stop. | |
| ... | |
| l.207 \usepackage | |
| {hyperref} | |
| ! ==> Fatal error occurred, no output PDF file produced! | |
| Transcript written on prisc.log. | |
| [verbose]: pdflatex 'prisc.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running pdflatex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && pdflatex 'prisc.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex) | |
| restricted \write18 enabled. | |
| entering extended mode | |
| (./prisc.tex | |
| LaTeX2e <2016/03/31> patch level 3 | |
| Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. | |
| (/texlive/2016/texmf-dist/tex/latex/acmart/acmart.cls | |
| Document Class: acmart 2016/11/16 v1.24 Typesetting articles for Association of | |
| Computing Machinery | |
| (/texlive/2016/texmf-dist/tex/latex/xkeyval/xkeyval.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/xkeyval.tex | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/xkvutils.tex | |
| (/texlive/2016/texmf-dist/tex/generic/xkeyval/keyval.tex)))) | |
| (/texlive/2016/texmf-dist/tex/latex/amscls/amsart.cls | |
| Document Class: amsart 2015/03/04 v2.20.2 | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsmath.sty | |
| For additional information on amsmath, use the `?' option. | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amstext.sty | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsgen.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsbsy.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsmath/amsopn.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype.sty | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype-pdftex.def) | |
| (/texlive/2016/texmf-dist/tex/latex/microtype/microtype.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/totpages/totpages.sty | |
| (/texlive/2016/texmf-dist/tex/latex/ms/everyshi.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/environ/environ.sty | |
| (/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty)) | |
| (/texlive/2016/texmf-local/tex/latex/natbib/natbib.sty | |
| This is natbib version 8.31 | |
| ************************************************************* | |
| !!WARNING!! !!WARNING!! !!WARNING!! !!WARNING!! | |
| This version (v8.31) of natbib is stricter in its formatting | |
| requirements for bibitem entries than the previous version | |
| used at arXiv (v7.1). | |
| If your submission encounters a problem see | |
| http://arXiv.org/help/faq/texlive | |
| and the natbib documentation at | |
| http://www.ctan.org/tex-archive/macros/latex/contrib/natbib/ | |
| for explanation and adjust your submission accordingly. | |
| The arXiv team. | |
| ************************************************************* | |
| ) (/texlive/2016/texmf-dist/tex/latex/hyperref/hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) | |
| (/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/auxhook.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/kvoptions.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/pd1enc.def) | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/hyperref.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/url/url.sty)) | |
| Package hyperref Message: Driver (autodetected): hpdftex. | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/hpdftex.def | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-def/pdftex.def))) | |
| (/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg) | |
| (/texlive/2016/texmf-dist/tex/latex/graphics/dvipsnam.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/geometry/geometry.sty | |
| (/texlive/2016/texmf-config/tex/latex/latexconfig/geometry.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/ncctools/manyfoot.sty | |
| (/texlive/2016/texmf-dist/tex/latex/ncctools/nccfoots.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/libertine.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def)) | |
| (/texlive/2016/texmf-dist/tex/latex/mweights/mweights.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fontaxes/fontaxes.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/LinLibertine_I.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/inconsolata/zi4.sty | |
| `inconsolata-zi4' v1.10, 2016/02/22 Text macros for Inconsolata (msharpe)) | |
| (/texlive/2016/texmf-dist/tex/latex/newtx/newtxmath.sty | |
| `newtxmath' v1.514, 2016/11/18 Math macros based on txfonts (msharpe) | |
| (/texlive/2016/texmf-dist/tex/generic/kastrup/binhex.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption.sty | |
| (/texlive/2016/texmf-dist/tex/latex/caption/caption3.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/float/float.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/comment/comment.sty | |
| Excluding comment 'comment') Excluding comment 'CCSXML' | |
| (/texlive/2016/texmf-arxiv/tex/latex/fancyhdr/fancyhdr.sty) | |
| Special comment 'acks' Include comment 'screenonly' | |
| Excluding comment 'printonly' Include comment 'anonsuppress' | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/OT1LinuxLibertineT-TLF.fd)) | |
| (/texlive/2016/texmf-dist/tex/latex/booktabs/booktabs.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/caption/subcaption.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/semantic.sty | |
| Semantic Package v2.0(epsilon) [2003/10/28] | |
| CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ | |
| Loading features: | |
| (/texlive/2016/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, | |
| and general definitions. | |
| ) (/texlive/2016/texmf-dist/tex/latex/mathpartir/mathpartir.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/xspace.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/latexsym.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mathtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tools/calc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/mathtools/mhsetup.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.sty | |
| (/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg)) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/verbatim.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.c | |
| ode.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex | |
| ) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmet | |
| ics.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code. | |
| tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.cod | |
| e.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.t | |
| ex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex)) | |
| ) (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty | |
| )) (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgffor.sty | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/pgf/math/pgfmath.sty | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code | |
| .tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arytopaths.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypositioning.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshadows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfadings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex) | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryarrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arycalc.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arybackgrounds.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryfit.code.tex) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.geometric.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geo | |
| metric.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.misc.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mis | |
| c.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.symbols.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.sym | |
| bols.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.arrows.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arr | |
| ows.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.callouts.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.cal | |
| louts.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| aryshapes.multipart.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.mul | |
| tipart.code.tex))) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.pathreplacing.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.pathreplacing.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arypatterns.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex | |
| )) | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibr | |
| arydecorations.markings.code.tex | |
| (/texlive/2016/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecor | |
| ations.markings.code.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikzscale/tikzscale.sty | |
| (/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/l3packages/xparse/xparse.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3.sty | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/expl3-code.tex) | |
| (/texlive/2016/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))) | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.sty | |
| (/texlive/2016/texmf-dist/tex/generic/xstring/xstring.tex))) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.sty | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgfsubpic.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/pgftree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/tikz-qtree/tikz-qtree.tex)) | |
| (/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty | |
| (/texlive/2016/texmf-dist/tex/latex/base/t1enc.def) | |
| (/texlive/2016/texmf-dist/tex/latex/libertine/T1LinuxLibertineT-TLF.fd)) | |
| (/texlive/2016/texmf-dist/tex/latex/bera/beramono.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/epigraph/epigraph.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/wrapfig/wrapfig.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/scalerel/scalerel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty | |
| (/texlive/2016/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/changepage/changepage.sty) (./coqed.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/tools/bm.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/cancel/cancel.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/oberdiek/centernot.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-restate.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thmtools.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-patch.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/parseargs.sty)) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-kv.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-autoref.sty | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/aliasctr.sty | |
| (/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-listof.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/thmtools/thm-amsthm.sty))) | |
| (/texlive/2016/texmf-dist/tex/latex/enumitem/enumitem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/fancyvrb/fancyvrb.sty | |
| Style option: `fancyvrb' v2.7a, with DG/SPQR fixes, and firstline=lastline fix | |
| <2008/02/07> (tvz)) (/texlive/2016/texmf-dist/tex/latex/varwidth/varwidth.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/combelow/combelow.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/bussproofs/bussproofs.sty | |
| Proof Tree (bussproofs) style macros. Version 1.1. | |
| ) (/texlive/2016/texmf-dist/tex/generic/ulem/ulem.sty) | |
| (/texlive/2016/texmf-dist/tex/latex/cleveref/cleveref.sty) (./cmds.tex | |
| ! LaTeX Error: \hole undefined. | |
| See the LaTeX manual or LaTeX Companion for explanation. | |
| Type H <return> for immediate help. | |
| ... | |
| l.133 \renewcommand{\hole} | |
| [1]{\ensuremath{\left[#1\right]}} | |
| ? | |
| ! Emergency stop. | |
| ... | |
| l.133 \renewcommand{\hole} | |
| [1]{\ensuremath{\left[#1\right]}} | |
| ! ==> Fatal error occurred, no output PDF file produced! | |
| Transcript written on prisc.log. | |
| [verbose]: pdflatex 'prisc.tex' failed. | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'prisc.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./prisc.tex | |
| ! Undefined control sequence. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| ? | |
| ! Emergency stop. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| No pages of output. | |
| Transcript written on prisc.log. | |
| [verbose]: tex 'prisc.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'prisc.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./prisc.tex | |
| ! Undefined control sequence. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| ? | |
| ! Emergency stop. | |
| l.1 \PassOptionsToPackage | |
| {names,dvipsnames}{xcolor} | |
| No pages of output. | |
| Transcript written on prisc.log. | |
| [verbose]: tex 'prisc.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'prisc.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'ANI.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'ANI.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./ANI.tex | |
| ! Undefined control sequence. | |
| l.13 correct compiler (\ccequal | |
| ) is enough to ensure the preservation of | |
| ? | |
| ! Emergency stop. | |
| l.13 correct compiler (\ccequal | |
| ) is enough to ensure the preservation of | |
| No pages of output. | |
| Transcript written on ANI.log. | |
| [verbose]: tex 'ANI.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'ANI.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./ANI.tex | |
| ! Undefined control sequence. | |
| l.13 correct compiler (\ccequal | |
| ) is enough to ensure the preservation of | |
| ? | |
| ! Emergency stop. | |
| l.13 correct compiler (\ccequal | |
| ) is enough to ensure the preservation of | |
| No pages of output. | |
| Transcript written on ANI.log. | |
| [verbose]: tex 'ANI.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'ANI.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'app-proofs-marco-statements.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'app-proofs-marco-statements.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./app-proofs-marco-statements.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Elided Formalization Bits}\label{sec:elided} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Elided Formalization Bits}\label{sec:elided} | |
| No pages of output. | |
| Transcript written on app-proofs-marco-statements.log. | |
| [verbose]: tex 'app-proofs-marco-statements.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'app-proofs-marco-statements.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./app-proofs-marco-statements.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Elided Formalization Bits}\label{sec:elided} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Elided Formalization Bits}\label{sec:elided} | |
| No pages of output. | |
| Transcript written on app-proofs-marco-statements.log. | |
| [verbose]: tex 'app-proofs-marco-statements.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'app-proofs-marco-statements.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'app-proofs-marco.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'app-proofs-marco.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./app-proofs-marco.tex | |
| ! Undefined control sequence. | |
| l.4 \section | |
| {Proofs for \Cref{SEC:MARCO}}\label{sec:proofs-marco} | |
| ? | |
| ! Emergency stop. | |
| l.4 \section | |
| {Proofs for \Cref{SEC:MARCO}}\label{sec:proofs-marco} | |
| No pages of output. | |
| Transcript written on app-proofs-marco.log. | |
| [verbose]: tex 'app-proofs-marco.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'app-proofs-marco.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./app-proofs-marco.tex | |
| ! Undefined control sequence. | |
| l.4 \section | |
| {Proofs for \Cref{SEC:MARCO}}\label{sec:proofs-marco} | |
| ? | |
| ! Emergency stop. | |
| l.4 \section | |
| {Proofs for \Cref{SEC:MARCO}}\label{sec:proofs-marco} | |
| No pages of output. | |
| Transcript written on app-proofs-marco.log. | |
| [verbose]: tex 'app-proofs-marco.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'app-proofs-marco.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'appendix-other.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'appendix-other.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./appendix-other.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Preserving Other (Hyper)Property Classes} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Preserving Other (Hyper)Property Classes} | |
| No pages of output. | |
| Transcript written on appendix-other.log. | |
| [verbose]: tex 'appendix-other.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'appendix-other.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./appendix-other.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Preserving Other (Hyper)Property Classes} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Preserving Other (Hyper)Property Classes} | |
| No pages of output. | |
| Transcript written on appendix-other.log. | |
| [verbose]: tex 'appendix-other.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'appendix-other.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'cmds.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'cmds.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./cmds.tex | |
| ! Undefined control sequence. | |
| l.10 \newcommand | |
| {\MP}[1]{\marco{#1}} | |
| ? | |
| ! Emergency stop. | |
| l.10 \newcommand | |
| {\MP}[1]{\marco{#1}} | |
| No pages of output. | |
| Transcript written on cmds.log. | |
| [verbose]: tex 'cmds.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'cmds.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./cmds.tex | |
| ! Undefined control sequence. | |
| l.10 \newcommand | |
| {\MP}[1]{\marco{#1}} | |
| ? | |
| ! Emergency stop. | |
| l.10 \newcommand | |
| {\MP}[1]{\marco{#1}} | |
| No pages of output. | |
| Transcript written on cmds.log. | |
| [verbose]: tex 'cmds.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'cmds.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'composition-appendix.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'composition-appendix.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./composition-appendix.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Composition results} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Composition results} | |
| No pages of output. | |
| Transcript written on composition-appendix.log. | |
| [verbose]: tex 'composition-appendix.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'composition-appendix.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./composition-appendix.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Composition results} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Composition results} | |
| No pages of output. | |
| Transcript written on composition-appendix.log. | |
| [verbose]: tex 'composition-appendix.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'composition-appendix.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'criteria.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'criteria.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./criteria.tex | |
| ! Undefined control sequence. | |
| l.1 \section | |
| {Robust Part} \ca{just temporary title} | |
| ? | |
| ! Emergency stop. | |
| l.1 \section | |
| {Robust Part} \ca{just temporary title} | |
| No pages of output. | |
| Transcript written on criteria.log. | |
| [verbose]: tex 'criteria.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'criteria.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./criteria.tex | |
| ! Undefined control sequence. | |
| l.1 \section | |
| {Robust Part} \ca{just temporary title} | |
| ? | |
| ! Emergency stop. | |
| l.1 \section | |
| {Robust Part} \ca{just temporary title} | |
| No pages of output. | |
| Transcript written on criteria.log. | |
| [verbose]: tex 'criteria.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'criteria.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-cc-only.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-cc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-cc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {figure}[!ht] | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {figure}[!ht] | |
| No pages of output. | |
| Transcript written on diagram-cc-only.log. | |
| [verbose]: tex 'diagram-cc-only.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-cc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-cc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {figure}[!ht] | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {figure}[!ht] | |
| No pages of output. | |
| Transcript written on diagram-cc-only.log. | |
| [verbose]: tex 'diagram-cc-only.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-cc-only.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-hc-only.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-hc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-hc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-hc-only.log. | |
| [verbose]: tex 'diagram-hc-only.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-hc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-hc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-hc-only.log. | |
| [verbose]: tex 'diagram-hc-only.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-hc-only.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-prop-pres-comp-corr.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-prop-pres-comp-corr.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-prop-pres-comp-corr.tex | |
| ! Undefined control sequence. | |
| l.2 \begin | |
| {figure}[!ht] | |
| ? | |
| ! Emergency stop. | |
| l.2 \begin | |
| {figure}[!ht] | |
| No pages of output. | |
| Transcript written on diagram-prop-pres-comp-corr.log. | |
| [verbose]: tex 'diagram-prop-pres-comp-corr.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-prop-pres-comp-corr.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-prop-pres-comp-corr.tex | |
| ! Undefined control sequence. | |
| l.2 \begin | |
| {figure}[!ht] | |
| ? | |
| ! Emergency stop. | |
| l.2 \begin | |
| {figure}[!ht] | |
| No pages of output. | |
| Transcript written on diagram-prop-pres-comp-corr.log. | |
| [verbose]: tex 'diagram-prop-pres-comp-corr.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-prop-pres-comp-corr.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-prop-pres-comp-security.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-prop-pres-comp-security.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-prop-pres-comp-security.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {figure}[!t] | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {figure}[!t] | |
| No pages of output. | |
| Transcript written on diagram-prop-pres-comp-security.log. | |
| [verbose]: tex 'diagram-prop-pres-comp-security.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-prop-pres-comp-security.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-prop-pres-comp-security.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {figure}[!t] | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {figure}[!t] | |
| No pages of output. | |
| Transcript written on diagram-prop-pres-comp-security.log. | |
| [verbose]: tex 'diagram-prop-pres-comp-security.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-prop-pres-comp-security.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-rtc-only.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-rtc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-rtc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-rtc-only.log. | |
| [verbose]: tex 'diagram-rtc-only.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-rtc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-rtc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-rtc-only.log. | |
| [verbose]: tex 'diagram-rtc-only.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-rtc-only.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram-sc-only.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-sc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-sc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-sc-only.log. | |
| [verbose]: tex 'diagram-sc-only.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram-sc-only.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram-sc-only.tex | |
| ! Undefined control sequence. | |
| l.3 \begin | |
| {center} | |
| ? | |
| ! Emergency stop. | |
| l.3 \begin | |
| {center} | |
| No pages of output. | |
| Transcript written on diagram-sc-only.log. | |
| [verbose]: tex 'diagram-sc-only.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram-sc-only.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diagram.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram.tex | |
| ! Undefined control sequence. | |
| l.1 \begin | |
| {figure} | |
| ? | |
| ! Emergency stop. | |
| l.1 \begin | |
| {figure} | |
| No pages of output. | |
| Transcript written on diagram.log. | |
| [verbose]: tex 'diagram.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diagram.tex | |
| ! Undefined control sequence. | |
| l.1 \begin | |
| {figure} | |
| ? | |
| ! Emergency stop. | |
| l.1 \begin | |
| {figure} | |
| No pages of output. | |
| Transcript written on diagram.log. | |
| [verbose]: tex 'diagram.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diagram.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diff_traces.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diff_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diff_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| No pages of output. | |
| Transcript written on diff_traces.log. | |
| [verbose]: tex 'diff_traces.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diff_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diff_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| No pages of output. | |
| Transcript written on diff_traces.log. | |
| [verbose]: tex 'diff_traces.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diff_traces.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'diff_values.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diff_values.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diff_values.tex | |
| ! Undefined control sequence. | |
| l.31 expressions \src | |
| {e} include naturals \src{n}, booleans \src{b}, conditi... | |
| ? | |
| ! Emergency stop. | |
| l.31 expressions \src | |
| {e} include naturals \src{n}, booleans \src{b}, conditi... | |
| No pages of output. | |
| Transcript written on diff_values.log. | |
| [verbose]: tex 'diff_values.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'diff_values.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./diff_values.tex | |
| ! Undefined control sequence. | |
| l.31 expressions \src | |
| {e} include naturals \src{n}, booleans \src{b}, conditi... | |
| ? | |
| ! Emergency stop. | |
| l.31 expressions \src | |
| {e} include naturals \src{n}, booleans \src{b}, conditi... | |
| No pages of output. | |
| Transcript written on diff_values.log. | |
| [verbose]: tex 'diff_values.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'diff_values.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'expand-sec-diagram.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'expand-sec-diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./expand-sec-diagram.tex | |
| ! Undefined control sequence. | |
| l.2 \citet | |
| {AbateBGHPT19} propose many more equivalent pairs of criteria, | |
| ? | |
| ! Emergency stop. | |
| l.2 \citet | |
| {AbateBGHPT19} propose many more equivalent pairs of criteria, | |
| No pages of output. | |
| Transcript written on expand-sec-diagram.log. | |
| [verbose]: tex 'expand-sec-diagram.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'expand-sec-diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./expand-sec-diagram.tex | |
| ! Undefined control sequence. | |
| l.2 \citet | |
| {AbateBGHPT19} propose many more equivalent pairs of criteria, | |
| ? | |
| ! Emergency stop. | |
| l.2 \citet | |
| {AbateBGHPT19} propose many more equivalent pairs of criteria, | |
| No pages of output. | |
| Transcript written on expand-sec-diagram.log. | |
| [verbose]: tex 'expand-sec-diagram.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'expand-sec-diagram.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'instance-marco-inputs.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-marco-inputs.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-marco-inputs.tex | |
| ! Undefined control sequence. | |
| l.2 \subsubsection | |
| {Possible Extensions: Inputs} | |
| ? | |
| ! Emergency stop. | |
| l.2 \subsubsection | |
| {Possible Extensions: Inputs} | |
| No pages of output. | |
| Transcript written on instance-marco-inputs.log. | |
| [verbose]: tex 'instance-marco-inputs.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-marco-inputs.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-marco-inputs.tex | |
| ! Undefined control sequence. | |
| l.2 \subsubsection | |
| {Possible Extensions: Inputs} | |
| ? | |
| ! Emergency stop. | |
| l.2 \subsubsection | |
| {Possible Extensions: Inputs} | |
| No pages of output. | |
| Transcript written on instance-marco-inputs.log. | |
| [verbose]: tex 'instance-marco-inputs.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'instance-marco-inputs.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'instance-marcodeepak.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-marcodeepak.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-marcodeepak.tex | |
| ! Undefined control sequence. | |
| l.3 \label | |
| {sec:example-more-events} | |
| ? | |
| ! Emergency stop. | |
| l.3 \label | |
| {sec:example-more-events} | |
| No pages of output. | |
| Transcript written on instance-marcodeepak.log. | |
| [verbose]: tex 'instance-marcodeepak.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-marcodeepak.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-marcodeepak.tex | |
| ! Undefined control sequence. | |
| l.3 \label | |
| {sec:example-more-events} | |
| ? | |
| ! Emergency stop. | |
| l.3 \label | |
| {sec:example-more-events} | |
| No pages of output. | |
| Transcript written on instance-marcodeepak.log. | |
| [verbose]: tex 'instance-marcodeepak.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'instance-marcodeepak.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'instance-more-target-statements.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-more-target-statements.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-more-target-statements.tex | |
| ! Undefined control sequence. | |
| l.7 ... pairs of arbitrary size, and a pure, \emph | |
| {untyped} target language | |
| ? | |
| ! Emergency stop. | |
| l.7 ... pairs of arbitrary size, and a pure, \emph | |
| {untyped} target language | |
| No pages of output. | |
| Transcript written on instance-more-target-statements.log. | |
| [verbose]: tex 'instance-more-target-statements.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-more-target-statements.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-more-target-statements.tex | |
| ! Undefined control sequence. | |
| l.7 ... pairs of arbitrary size, and a pure, \emph | |
| {untyped} target language | |
| ? | |
| ! Emergency stop. | |
| l.7 ... pairs of arbitrary size, and a pure, \emph | |
| {untyped} target language | |
| No pages of output. | |
| Transcript written on instance-more-target-statements.log. | |
| [verbose]: tex 'instance-more-target-statements.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'instance-more-target-statements.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'instance-more-target.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-more-target.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-more-target.tex | |
| ! Undefined control sequence. | |
| l.6 ...urce has a single action of the form \sends | |
| {v1,v2,v3}, which means to... | |
| ? | |
| ! Emergency stop. | |
| l.6 ...urce has a single action of the form \sends | |
| {v1,v2,v3}, which means to... | |
| No pages of output. | |
| Transcript written on instance-more-target.log. | |
| [verbose]: tex 'instance-more-target.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'instance-more-target.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./instance-more-target.tex | |
| ! Undefined control sequence. | |
| l.6 ...urce has a single action of the form \sends | |
| {v1,v2,v3}, which means to... | |
| ? | |
| ! Emergency stop. | |
| l.6 ...urce has a single action of the form \sends | |
| {v1,v2,v3}, which means to... | |
| No pages of output. | |
| Transcript written on instance-more-target.log. | |
| [verbose]: tex 'instance-more-target.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'instance-more-target.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'intro.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'intro.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./intro.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Introduction}\label{sec:intro} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Introduction}\label{sec:intro} | |
| No pages of output. | |
| Transcript written on intro.log. | |
| [verbose]: tex 'intro.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'intro.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./intro.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Introduction}\label{sec:intro} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Introduction}\label{sec:intro} | |
| No pages of output. | |
| Transcript written on intro.log. | |
| [verbose]: tex 'intro.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'intro.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'mappings.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'mappings.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./mappings.tex | |
| ! Undefined control sequence. | |
| l.3 As explained in \autoref | |
| {sec:intro}, trace-relating compiler correctness | |
| ? | |
| ! Emergency stop. | |
| l.3 As explained in \autoref | |
| {sec:intro}, trace-relating compiler correctness | |
| No pages of output. | |
| Transcript written on mappings.log. | |
| [verbose]: tex 'mappings.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'mappings.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./mappings.tex | |
| ! Undefined control sequence. | |
| l.3 As explained in \autoref | |
| {sec:intro}, trace-relating compiler correctness | |
| ? | |
| ! Emergency stop. | |
| l.3 As explained in \autoref | |
| {sec:intro}, trace-relating compiler correctness | |
| No pages of output. | |
| Transcript written on mappings.log. | |
| [verbose]: tex 'mappings.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'mappings.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'old-sc-diagram.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'old-sc-diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./old-sc-diagram.tex | |
| ! Undefined control sequence. | |
| l.4 ...strative diagram of the criteria from \cite | |
| {AbateBGHPT19} that are br... | |
| ? | |
| ! Emergency stop. | |
| l.4 ...strative diagram of the criteria from \cite | |
| {AbateBGHPT19} that are br... | |
| No pages of output. | |
| Transcript written on old-sc-diagram.log. | |
| [verbose]: tex 'old-sc-diagram.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'old-sc-diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./old-sc-diagram.tex | |
| ! Undefined control sequence. | |
| l.4 ...strative diagram of the criteria from \cite | |
| {AbateBGHPT19} that are br... | |
| ? | |
| ! Emergency stop. | |
| l.4 ...strative diagram of the criteria from \cite | |
| {AbateBGHPT19} that are br... | |
| No pages of output. | |
| Transcript written on old-sc-diagram.log. | |
| [verbose]: tex 'old-sc-diagram.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'old-sc-diagram.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'other_works.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'other_works.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./other_works.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Relation to Melton et al. and Sabry and Wadler} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Relation to Melton et al. and Sabry and Wadler} | |
| No pages of output. | |
| Transcript written on other_works.log. | |
| [verbose]: tex 'other_works.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'other_works.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./other_works.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Relation to Melton et al. and Sabry and Wadler} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Relation to Melton et al. and Sabry and Wadler} | |
| No pages of output. | |
| Transcript written on other_works.log. | |
| [verbose]: tex 'other_works.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'other_works.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'proofindex.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'proofindex.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./proofindex.tex | |
| ! Undefined control sequence. | |
| l.3 \section | |
| {Proof Index}\label{sec:pi} | |
| ? | |
| ! Emergency stop. | |
| l.3 \section | |
| {Proof Index}\label{sec:pi} | |
| No pages of output. | |
| Transcript written on proofindex.log. | |
| [verbose]: tex 'proofindex.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'proofindex.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./proofindex.tex | |
| ! Undefined control sequence. | |
| l.3 \section | |
| {Proof Index}\label{sec:pi} | |
| ? | |
| ! Emergency stop. | |
| l.3 \section | |
| {Proof Index}\label{sec:pi} | |
| No pages of output. | |
| Transcript written on proofindex.log. | |
| [verbose]: tex 'proofindex.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'proofindex.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'rel_to_maps.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'rel_to_maps.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./rel_to_maps.tex | |
| ! Undefined control sequence. | |
| <recently read> \cctilde | |
| l.3 ... investigate the relation between $\cctilde | |
| $ and | |
| ? | |
| ! Emergency stop. | |
| <recently read> \cctilde | |
| l.3 ... investigate the relation between $\cctilde | |
| $ and | |
| No pages of output. | |
| Transcript written on rel_to_maps.log. | |
| [verbose]: tex 'rel_to_maps.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'rel_to_maps.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./rel_to_maps.tex | |
| ! Undefined control sequence. | |
| <recently read> \cctilde | |
| l.3 ... investigate the relation between $\cctilde | |
| $ and | |
| ? | |
| ! Emergency stop. | |
| <recently read> \cctilde | |
| l.3 ... investigate the relation between $\cctilde | |
| $ and | |
| No pages of output. | |
| Transcript written on rel_to_maps.log. | |
| [verbose]: tex 'rel_to_maps.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'rel_to_maps.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'relating_src_trg_traces.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'relating_src_trg_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./relating_src_trg_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \ch | |
| {Need better motivation here, wasn't convinced by next paragraph} | |
| ? | |
| ! Emergency stop. | |
| l.2 \ch | |
| {Need better motivation here, wasn't convinced by next paragraph} | |
| No pages of output. | |
| Transcript written on relating_src_trg_traces.log. | |
| [verbose]: tex 'relating_src_trg_traces.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'relating_src_trg_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./relating_src_trg_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \ch | |
| {Need better motivation here, wasn't convinced by next paragraph} | |
| ? | |
| ! Emergency stop. | |
| l.2 \ch | |
| {Need better motivation here, wasn't convinced by next paragraph} | |
| No pages of output. | |
| Transcript written on relating_src_trg_traces.log. | |
| [verbose]: tex 'relating_src_trg_traces.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'relating_src_trg_traces.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'resource-exhaustion.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'resource-exhaustion.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./resource-exhaustion.tex | |
| ! Undefined control sequence. | |
| l.4 \autoref | |
| {sec:intro}. | |
| ? | |
| ! Emergency stop. | |
| l.4 \autoref | |
| {sec:intro}. | |
| No pages of output. | |
| Transcript written on resource-exhaustion.log. | |
| [verbose]: tex 'resource-exhaustion.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'resource-exhaustion.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./resource-exhaustion.tex | |
| ! Undefined control sequence. | |
| l.4 \autoref | |
| {sec:intro}. | |
| ? | |
| ! Emergency stop. | |
| l.4 \autoref | |
| {sec:intro}. | |
| No pages of output. | |
| Transcript written on resource-exhaustion.log. | |
| [verbose]: tex 'resource-exhaustion.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'resource-exhaustion.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'rob-diff-acts.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'rob-diff-acts.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./rob-diff-acts.tex | |
| ! Undefined control sequence. | |
| l.3 \rb | |
| {Now I have to clean and mostly remove the old text, relocating some ... | |
| ? | |
| ! Emergency stop. | |
| l.3 \rb | |
| {Now I have to clean and mostly remove the old text, relocating some ... | |
| No pages of output. | |
| Transcript written on rob-diff-acts.log. | |
| [verbose]: tex 'rob-diff-acts.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'rob-diff-acts.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./rob-diff-acts.tex | |
| ! Undefined control sequence. | |
| l.3 \rb | |
| {Now I have to clean and mostly remove the old text, relocating some ... | |
| ? | |
| ! Emergency stop. | |
| l.3 \rb | |
| {Now I have to clean and mostly remove the old text, relocating some ... | |
| No pages of output. | |
| Transcript written on rob-diff-acts.log. | |
| [verbose]: tex 'rob-diff-acts.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'rob-diff-acts.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'robust-trace.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust-trace.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust-trace.tex | |
| ! Undefined control sequence. | |
| l.14 \myparagraph | |
| {Source and Target Languages} | |
| ? | |
| ! Emergency stop. | |
| l.14 \myparagraph | |
| {Source and Target Languages} | |
| No pages of output. | |
| Transcript written on robust-trace.log. | |
| [verbose]: tex 'robust-trace.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust-trace.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust-trace.tex | |
| ! Undefined control sequence. | |
| l.14 \myparagraph | |
| {Source and Target Languages} | |
| ? | |
| ! Emergency stop. | |
| l.14 \myparagraph | |
| {Source and Target Languages} | |
| No pages of output. | |
| Transcript written on robust-trace.log. | |
| [verbose]: tex 'robust-trace.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'robust-trace.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'robust_diagram.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust_diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust_diagram.tex | |
| ! Undefined control sequence. | |
| l.1 \label | |
| {fig:robustdiffdiagram} | |
| ? | |
| ! Emergency stop. | |
| l.1 \label | |
| {fig:robustdiffdiagram} | |
| No pages of output. | |
| Transcript written on robust_diagram.log. | |
| [verbose]: tex 'robust_diagram.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust_diagram.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust_diagram.tex | |
| ! Undefined control sequence. | |
| l.1 \label | |
| {fig:robustdiffdiagram} | |
| ? | |
| ! Emergency stop. | |
| l.1 \label | |
| {fig:robustdiffdiagram} | |
| No pages of output. | |
| Transcript written on robust_diagram.log. | |
| [verbose]: tex 'robust_diagram.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'robust_diagram.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'robust_diff_traces.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust_diff_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust_diff_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| No pages of output. | |
| Transcript written on robust_diff_traces.log. | |
| [verbose]: tex 'robust_diff_traces.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'robust_diff_traces.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./robust_diff_traces.tex | |
| ! Undefined control sequence. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| ? | |
| ! Emergency stop. | |
| l.2 \section | |
| {Differing Source and Target Trace Models} | |
| No pages of output. | |
| Transcript written on robust_diff_traces.log. | |
| [verbose]: tex 'robust_diff_traces.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'robust_diff_traces.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'sec-comp-explain.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'sec-comp-explain.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./sec-comp-explain.tex | |
| ! Undefined control sequence. | |
| l.10 ... generalize many of the criteria of \citet | |
| {AbateBGHPT19} using | |
| ? | |
| ! Emergency stop. | |
| l.10 ... generalize many of the criteria of \citet | |
| {AbateBGHPT19} using | |
| No pages of output. | |
| Transcript written on sec-comp-explain.log. | |
| [verbose]: tex 'sec-comp-explain.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'sec-comp-explain.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./sec-comp-explain.tex | |
| ! Undefined control sequence. | |
| l.10 ... generalize many of the criteria of \citet | |
| {AbateBGHPT19} using | |
| ? | |
| ! Emergency stop. | |
| l.10 ... generalize many of the criteria of \citet | |
| {AbateBGHPT19} using | |
| No pages of output. | |
| Transcript written on sec-comp-explain.log. | |
| [verbose]: tex 'sec-comp-explain.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'sec-comp-explain.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'secure-compilation-motivation.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'secure-compilation-motivation.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./secure-compilation-motivation.tex | |
| ! Undefined control sequence. | |
| l.8 ...teract with other programs, libraries, \ETC | |
| ? | |
| ! Emergency stop. | |
| l.8 ...teract with other programs, libraries, \ETC | |
| No pages of output. | |
| Transcript written on secure-compilation-motivation.log. | |
| [verbose]: tex 'secure-compilation-motivation.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'secure-compilation-motivation.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./secure-compilation-motivation.tex | |
| ! Undefined control sequence. | |
| l.8 ...teract with other programs, libraries, \ETC | |
| ? | |
| ! Emergency stop. | |
| l.8 ...teract with other programs, libraries, \ETC | |
| No pages of output. | |
| Transcript written on secure-compilation-motivation.log. | |
| [verbose]: tex 'secure-compilation-motivation.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'secure-compilation-motivation.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'two_dot_one.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'two_dot_one.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./two_dot_one.tex | |
| ! Undefined control sequence. | |
| l.1 \subsection | |
| {Compiler Correctness} | |
| ? | |
| ! Emergency stop. | |
| l.1 \subsection | |
| {Compiler Correctness} | |
| No pages of output. | |
| Transcript written on two_dot_one.log. | |
| [verbose]: tex 'two_dot_one.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'two_dot_one.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./two_dot_one.tex | |
| ! Undefined control sequence. | |
| l.1 \subsection | |
| {Compiler Correctness} | |
| ? | |
| ! Emergency stop. | |
| l.1 \subsection | |
| {Compiler Correctness} | |
| No pages of output. | |
| Transcript written on two_dot_one.log. | |
| [verbose]: tex 'two_dot_one.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'two_dot_one.tex' | |
| [verbose]: ~~~~~~~~~~~ Processing file 'undefbeh.tex' | |
| [verbose]: 'htex' is not a valid TeX format; will ignore. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running htex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'undefbeh.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./undefbeh.tex | |
| ! Undefined control sequence. | |
| l.3 in \autoref | |
| {sec:intro}. | |
| ? | |
| ! Emergency stop. | |
| l.3 in \autoref | |
| {sec:intro}. | |
| No pages of output. | |
| Transcript written on undefbeh.log. | |
| [verbose]: tex 'undefbeh.tex' failed. | |
| [verbose]: TEXMFCNF is unset. | |
| [verbose]: ~~~~~~~~~~~ Running tex for the first time ~~~~~~~~ | |
| [verbose]: Running: "(export HOME=/tmp PATH=/texlive/2016/bin/arch:/bin; cd /submissions/3057447/ && tex 'undefbeh.tex' < /dev/null)" 2>&1 | |
| [verbose]: This is TeX, Version 3.14159265 (TeX Live 2016) (preloaded format=tex) | |
| (./undefbeh.tex | |
| ! Undefined control sequence. | |
| l.3 in \autoref | |
| {sec:intro}. | |
| ? | |
| ! Emergency stop. | |
| l.3 in \autoref | |
| {sec:intro}. | |
| No pages of output. | |
| Transcript written on undefbeh.log. | |
| [verbose]: tex 'undefbeh.tex' failed. | |
| [verbose]: We failed utterly to process the TeX file 'undefbeh.tex' | |
| [error]: Unable to sucessfully process tex files. | |
| *** AutoTeX ABORTING *** | |
| [verbose]: AutoTeX returned error: Unable to sucessfully process tex files. | |
| [verbose]: $autotex->process failed $@: $?: 0 $!: Inappropriate ioctl for device | |
| [verbose]: Error running AutoTeX process: |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment