[isabelle-dev] Unfinished session(s): Abstract_Completeness, Probabilistic_Noninterference

[Johannes Hölzl]

Fixed with 1bcf0828d38c and 7a2b867fa843.

Am Montag, den 17.11.2014, 09:13 +0100 schrieb Florian Haftmann:
> > 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
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev