Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Recurring error from Isabelle Syslog


view this post on Zulip Email Gateway (Apr 30 2021 at 14:52):

From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear list,

I am getting a recurring and annoying error from Isabelle Syslog. I am
getting this error mostly when I type LateX text inside the Isabelle/Isar
command *text. *


The error


Welcome to Isabelle/HOL (Isabelle2021: February 2021)
Interrupt
Interrupt
Interrupt
Interrupt
standard_error terminated
standard_output terminated
message_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 137 (KILL SIGNAL)


Here is my system config:


Distributor ID: Ubuntu
Description: Ubuntu 20.04.2 LTS
Release: 20.04
Codename: focal

thinkpad-t480s
description: Computer
width: 64 bits
capabilities: smp vsyscall32
*-core
description: Motherboard
physical id: 0
*-memory
description: System memory
physical id: 0
size: 15GiB
*-cpu
product: Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz
vendor: Intel Corp.
physical id: 1
bus info: cpu@0
size: 1327MHz
capacity: 4GHz
width: 64 bits
capabilities: fpu fpu_exception wp 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 x86-64 constant_tsc art arch_perfmon
pebs bts rep_good nopl xtopology nonstop_tsc cpuid aperfmperf 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 cpuid_fault epb invpcid_single pti ssbd ibrs ibpb
stibp tpr_shadow vnmi flexpriority ept vpid ept_ad fsgsbase tsc_adjust bmi1
avx2 smep bmi2 erms invpcid mpx rdseed adx smap clflushopt intel_pt
xsaveopt xsavec xgetbv1 xsaves dtherm ida arat pln pts hwp hwp_notify
hwp_act_window hwp_epp md_clear flush_l1d cpufreq

*-display
description: VGA compatible controller
product: UHD Graphics 620
vendor: Intel Corporation
physical id: 2
version: 07
width: 64 bits
clock: 33MHz
capabilities: vga_controller bus_master cap_list rom
configuration: driver=i915 latency=0
resources: irq:149 memory:e7000000-e7ffffff
memory:c0000000-cfffffff ioport:e000(size=64) memory:c0000-dffff
*-generic:0
description: Signal processing controller
product: Xeon E3-1200 v5/E3-1500 v5/6th Gen Core Processor
Thermal Subsystem
vendor: Intel Corporation
physical id: 4
version: 08
width: 64 bits
clock: 33MHz
capabilities: cap_list
configuration: driver=proc_thermal latency=0
resources: irq:16 memory:e8240000-e8247fff
*-generic:1 UNCLAIMED
description: System peripheral
product: Xeon E3-1200 v5/v6 / E3-1500 v5 / 6th/7th/8th Gen
Core Processor Gaussian

Best wishes,

Yakoub.

view this post on Zulip Email Gateway (Apr 30 2021 at 14:57):

From: Jakub Kądziołka <kuba@kadziolka.net>
Could this be caused by Isabelle falling prey to the OOM killer? Try to
reproduce this while observing memory usage.

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Apr 30 2021 at 14:58):

From: Peter Lammich <lammich@in.tum.de>
I get this when the out-of-memory killer reaps the PolyML process. Can
you examine your OS's syslog for anything mentioning OOM (dmesg on
Linux), no idea how to find it on other OSs. ALso check, shortly before
the error occurs, hoiw much memory Isabelle consumes.

view this post on Zulip Email Gateway (May 02 2021 at 10:15):

From: Makarius <makarius@sketis.net>
16 GB looks fine to me: I would not expect out-of-memory problems with it for
medium sized applications.

Here are some arbitrary links found within 5min:

https://linuxize.com/post/create-a-linux-swap-file

https://serverfault.com/questions/141988/avoid-linux-out-of-memory-application-teardown

Makarius

view this post on Zulip Email Gateway (May 02 2021 at 20:20):

From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear all,

Thank you all for the hints. From what I understood, to handle this I have
either to disable OOM killer or create swap space!

@Jakub and Peter: What was your solution? I tried to reproduce the
error but I have been falling for the last 2 days, it looks like
understanding the semantics of OOM killer is a bit complicated!

@Makarius: Thank you for the pointers, indeed very useful links. (BTW I am
not a windows user anymore, namely, I am not using VM to run Linux. I could
not survive in my research by using windows as soon as I started messing
around compilers front-end and backend!Therefore switched for Linux! I
merely use Windows to contribute to the tests of the newly launched
Isabelle App, so I launch up on my developments and report what I observe.)

Best wishes,

Yakoub.

view this post on Zulip Email Gateway (May 03 2021 at 12:04):

From: Peter Lammich <lammich@in.tum.de>

16 GB looks fine to me: I would not expect out-of-memory problems
with it for
medium sized applications.

What is medium-size?
the OOM regularly kills my Isabelle sessions on my 32GiB machine, when,
e.g., loading things like
https://www.isa-afp.org/browser_info/current/AFP/Prpu_Maxflow/Generated_Code_Test.html


Last updated: Dec 05 2021 at 22:18 UTC