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

[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



-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 266 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141117/244c457f/attachment.asc>