> isabelle: c48becd96398 tip
> afp: 45dd81cdecef tip
> Building HOL ...
> Finished HOL (0:01:56 elapsed time, 0:05:46 cpu time, factor 2.97)
> Building HOL-Word ...
> Finished HOL-Word (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.74)
> Building JinjaThreads ...
> JinjaThreads FAILED
> (see also
> /srv/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
> list
> *
> (Isabelle8115590.Generated_Code.nat *
> (Isabelle8115590.Generated_Code.nat * (string option * ...))
> )
> list))
> *
> (Isabelle8115590.Generated_Code.nat
> Isabelle8115590.Generated_Code.vala
> list
> *
> (Isabelle8115590.Generated_Code.nat
> Isabelle8115590.Generated_Code.vala
> list
> *
> (string * (string * Isabelle8115590.Generated_Code.nat))))
> )
> list)
> *
> (Isabelle8115590.Generated_Code.nat, Isabelle8115590.Generated_Code.nat
> )
> Isabelle8115590.Generated_Code.finfun
> )
> Isabelle8115590.Generated_Code.rbt
> *
> (Isabelle8115590.Generated_Code.nat,
> Isabelle8115590.Generated_Code.heapobj)
> Isabelle8115590.Generated_Code.rbt)
> *
> ((Isabelle8115590.Generated_Code.nat,
> Isabelle8115590.Generated_Code.nat
> Isabelle8115590.Generated_Code.wait_set_status
> )
> Isabelle8115590.Generated_Code.rbt
> *
> (Isabelle8115590.Generated_Code.nat, unit)
> Isabelle8115590.Generated_Code.rbt))
> )
> Isabelle8115590.Generated_Code.tllist
> *** exception SysErr ("Cannot allocate memory", SOME ENOMEM) raised (line 83
> of "./basis/PolyMLException.sml")
> Unfinished session(s): JinjaThreads
> 0:32:24 elapsed time, 1:54:58 cpu time, factor 3.55
JinjaThreads with regular PolyML finishes within about 30 minutes.
Relevant hardware data might include:
> $ lscpu
> Architecture: x86_64
> CPU op-mode(s): 32-bit, 64-bit
> Byte Order: Little Endian
> CPU(s): 8
> On-line CPU(s) list: 0-7
> Thread(s) pro Kern: 2
> Kern(e) pro Socket: 4
> Socket(s): 1
> NUMA-Knoten: 1
> Anbieterkennung: GenuineIntel
> Prozessorfamilie: 6
> Modell: 94
> Model name: Intel(R) Core(TM) i7-6700K CPU @ 4.00GHz
> Stepping: 3
> CPU MHz: 800.000
> CPU max MHz: 4200,0000
> CPU min MHz: 800,0000
> BogoMIPS: 8015.87
> Virtualisierung: VT-x
> L1d Cache: 32K
> L1i Cache: 32K
> L2 Cache: 256K
> L3 Cache: 8192K
> NUMA node0 CPU(s): 0-7
> Flags: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge
> mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx
> pdpe1gb rdtscp lm constant_tsc art arch_perfmon pebs bts rep_good nopl
> xtopology nonstop_tsc aperfmperf eagerfpu pni pclmulqdq dtes64 monitor ds_cpl
> vmx est tm2 ssse3 sdbg fma cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic movbe
> popcnt tsc_deadline_timer aes xsave avx f16c rdrand lahf_lm abm 3dnowprefetch
> epb intel_pt tpr_shadow vnmi flexpriority ept vpid fsgsbase tsc_adjust bmi1
> hle avx2 smep bmi2 erms invpcid rtm mpx rdseed adx smap clflushopt xsaveopt
> xsavec xgetbv1 dtherm ida arat pln pts hwp hwp_notify hwp_act_window hwp_epp
> $ free
> total used free shared buff/cache
> available
> Mem: 16099596 1355396 12329292 265960 2414908
> 14110560
> Swap: 8388604 0 8388604
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
