> 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