[isabelle-dev] [Isabelle-ci] Build failure in Isabelle+AFP (slow)
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Mar 14 13:39:08 CET 2019
I'm note sure what's going on here.
It appears to be a spontaneous dropout of the OCaml environment,
sporadically: in session Native_Word, theory
~~/afp/thys/Native_Word/Bits_Integer.thy seems to success, whereas in
e.g. Iptables_Semantics it fails.
I did not experience anything like that on lxcisa0 with -j 6 and the
latest polyml 5.8 rc (!).
ML_PLATFORM="x86_64_32-linux"
ML_OPTIONS="--minheap 500"
Are there any other clues to have a look for?
Cheers,
Florian
Am 14.03.19 um 12:38 schrieb Isabelle/Jenkins:
> Iptables_Semantics FAILED
> (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.8_x86_64-linux/log/Iptables_Semantics)
> Loading theory "Iptables_Semantics.Semantics_Embeddings"
> ### theory "Iptables_Semantics.Semantics_Embeddings"
> ### 1.148s elapsed time, 8.876s cpu time, 0.168s GC time
> Loading theory "Iptables_Semantics.Access_Matrix_Embeddings"
> Loading theory "Iptables_Semantics.Iptables_Semantics"
> ### theory "Iptables_Semantics.Iptables_Semantics"
> ### 0.078s elapsed time, 0.616s cpu time, 0.000s GC time
> Loading theory "Iptables_Semantics.No_Spoof_Embeddings"
> "False"
> :: "bool"
> ### theory "Iptables_Semantics.No_Spoof_Embeddings"
> ### 0.192s elapsed time, 1.524s cpu time, 0.000s GC time
> ### theory "Iptables_Semantics.Access_Matrix_Embeddings"
> ### 0.966s elapsed time, 6.944s cpu time, 0.300s GC time
> (\<And>r m.
> \<lbrakk>r \<in> set ?rs; ?f (get_match r) = Some m\<rbrakk>
> \<Longrightarrow> normalized_nnf_match m \<and>
> \<not> has_disc_negated disc3 False m \<and>
> P m) \<Longrightarrow>
> \<forall>r\<in>set (optimize_matches_option ?f ?rs).
> normalized_nnf_match (get_match r) \<and>
> \<not> has_disc_negated disc3 False (get_match r) \<and> P (get_match r)
> \<lbrakk>\<forall>r\<in>set ?rs.
> normalized_nnf_match (get_match r) \<and>
> \<not> has_disc_negated disc3 False (get_match r);
> \<forall>m.
> normalized_nnf_match m \<and>
> \<not> has_disc_negated disc3 False m \<longrightarrow>
> (\<forall>m'\<in>set (?f m). ?Q m')\<rbrakk>
> \<Longrightarrow> \<forall>r\<in>set (normalize_rules ?f ?rs).
> ?Q (get_match r)
> isabelle document -d /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document -o pdf -n document
> isabelle document -d /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline -o pdf -n outline -t /proof,/ML
> *** Failed to load theory "Native_Word.Code_Target_Bits_Int" (unresolved "Native_Word.Bits_Integer")
> *** Failed to load theory "Iptables_Semantics.Code_Interface" (unresolved "Native_Word.Code_Target_Bits_Int")
> *** Failed to load theory "Iptables_Semantics.Parser" (unresolved "Iptables_Semantics.Code_Interface")
> *** Failed to load theory "Iptables_Semantics.Code_haskell" (unresolved "Iptables_Semantics.Parser")
> *** Failed to load theory "Iptables_Semantics.Documentation" (unresolved "Iptables_Semantics.Code_Interface")
> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
> *** At command "export_code" (line 630 of "~~/afp/thys/Native_Word/Bits_Integer.thy")
> Iptables_Semantics_Examples CANCELLED
> Iptables_Semantics_Examples_Big CANCELLED
> Unfinished session(s): ConcurrentGC, ConcurrentIMP, HOL-Library, Iptables_Semantics, Iptables_Semantics_Examples, Iptables_Semantics_Examples_Big, JinjaThreads
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190314/a1eb5050/attachment.asc>
More information about the isabelle-dev
mailing list