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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
