[isabelle-dev] [Isabelle-ci] Build failure in Isabelle+AFP (slow)

[Florian Haftmann]

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>