> isabelle: 059ba950a657 tip > afp: 0fdf8f639bb4 tip > Building HOL-Multivariate_Analysis ... > Running Sturm_Tarski ... > Running Abstract_Completeness ... > Finished Sturm_Tarski (0:00:28 elapsed time, 0:01:21 cpu time, factor 2.89) > > Abstract_Completeness FAILED > (see also > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Abstract_Completeness) > > > [20] [21] [22] [23] [24] [25]) (./Abstract_Completeness.tex) > (./Propositional_Logic.tex [26] [27])) [28] (./root.aux) ) > (see the transcript file for additional > information)</usr/share/texmf-dist/font > s/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texmf-dist/fonts/type1/public > /amsfonts/cm/cmbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c > mex10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-d > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1 > /public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/fonts/type1/public/amsfont > s/cm/cmr7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb> > </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/tex > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb> > Output written on root.pdf (28 pages, 198420 bytes). > Transcript written on root.log. > > *** Failed to apply terminal proof method (line 128 of > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy"): > *** goal (1 subgoal): > *** 1. ev (holds (op = r)) (rs @- flat (smap (%n. stake n rules) (fromN n))) > *** At command "qed" (line 128 of > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy") > Finished HOL-Multivariate_Analysis (0:03:18 elapsed time, 0:10:58 cpu time, > factor 3.32) > Building HOL-Probability ... > Finished HOL-Probability (0:03:20 elapsed time, 0:11:32 cpu time, factor 3.46) > Running Probabilistic_Noninterference ... > > Probabilistic_Noninterference FAILED > (see also > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Probabilistic_Noninterference) > > mr/m/n/10 )$ \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 c1 $\OMS/cmsy/m/n/10 > ^^Y$\ > OT1/cmr/m/it/10 01 c2 $\OMS/cmsy/m/n/10 ^^Q$ $\OT1/cmr/m/n/10 > ($\OT1/cmr/m/it/1 > 0 c1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 c2$\OT1/cmr/m/n/10 )$ > $\OMS/cmsy/m/n/1 > 0 2$ \OT1/cmr/m/it/10 Example[]PL$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 ZObis[] > [69])) (./root.bbl) [70] (./root.aux) ) > (see the transcript file for additional > information)</usr/share/texmf-dist/font > s/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texmf-dist/fonts/type1/public > /amsfonts/cm/cmbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c > mex10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-d > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1 > /public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/fonts/type1/public/amsfont > s/cm/cmr6.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb> > </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/tex > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb> > Output written on root.pdf (70 pages, 254440 bytes). > Transcript written on root.log. > > *** Undefined constant: "T.hitting_time" (line 235 of > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy") > *** At command "abbreviation" (line 235 of > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy") > Unfinished session(s): Abstract_Completeness, Probabilistic_Noninterference > 0:08:36 elapsed time, 0:33:24 cpu time, factor 3.88
-- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev