Email Gateway (Aug 18 2022 at 17:37): Email Gateway (Aug 18 2022 at 17:37):From: David Brumley <dbrumley@cmu.edu>
Hi,
I downloaded isabelle today for OS X from the main website
(Isabelle2011.dmg). I'm working through the tutorial at
http://isabelle.in.tum.de/doc/tutorial.pdf. On page 20, I go to enter
in the type declaration given, using
\<not>
for the negation in the "value" method (per appendix A.1). Emacs
reliably crashes every time I do this. Crash report below.
What would be the best course of action to move forward? Install
carbon emacs 22.x? Use some other symbol entry for negation (what
would I use?)
Thanks,
David
Process: Emacs [62639]
Path:
/Applications/Isabelle2011.app/Contents/Resources/Emacs.app/Contents/MacOS/Emacs
Identifier: org.gnu.Emacs
Version: Version 23.2 (9.0)
Code Type: X86-64 (Native)
Parent Process: bash [62631]
Date/Time: 2011-04-25 11:16:16.359 -0400
OS Version: Mac OS X 10.6.7 (10J869)
Report Version: 6
Interval Since Last Report: 2506101 sec
Crashes Since Last Report: 11
Per-App Interval Since Last Report: 3565 sec
Per-App Crashes Since Last Report: 3
Anonymous UUID: 6B212705-6B54-44EC-8BE3-2EEC5563842D
Exception Type: EXC_CRASH (SIGABRT)
Exception Codes: 0x0000000000000000, 0x0000000000000000
Crashed Thread: 0 Dispatch queue: com.apple.main-thread
Application Specific Information:
abort() called
Thread 0 Crashed: Dispatch queue: com.apple.main-thread
0 libSystem.B.dylib 0x00007fff8020a5d6 __kill + 10
1 libSystem.B.dylib 0x00007fff802aacd6 abort + 83
2 org.gnu.Emacs 0x000000010016e44c ns_term_shutdown + 44
3 org.gnu.Emacs 0x0000000100090274 fatal_error_signal + 340
4 libSystem.B.dylib 0x00007fff8021c66a _sigtramp + 26
5 libSystem.B.dylib 0x00007fff8020a5d6 __kill + 10
6 libSystem.B.dylib 0x00007fff802aacd6 abort + 83
7 org.gnu.Emacs 0x00000001000bdd95
buf_charpos_to_bytepos + 389
8 org.gnu.Emacs 0x0000000100160a7b
composition_update_it + 539
9 org.gnu.Emacs 0x000000010002eca3
next_element_from_composition + 131
10 org.gnu.Emacs 0x000000010002f0b6
next_element_from_buffer + 182
11 org.gnu.Emacs 0x000000010002f235
next_element_from_buffer + 565
12 org.gnu.Emacs 0x000000010002bc90
get_next_display_element + 64
13 org.gnu.Emacs 0x0000000100032aba display_line + 474
14 org.gnu.Emacs 0x000000010003d313 try_window + 163
15 org.gnu.Emacs 0x000000010003f009 redisplay_window + 6713
16 org.gnu.Emacs 0x0000000100040847 redisplay_window_0 + 39
17 org.gnu.Emacs 0x00000001001075ae
internal_condition_case_1 + 334
18 org.gnu.Emacs 0x0000000100029a9d redisplay_windows + 93
19 org.gnu.Emacs 0x000000010004148c redisplay_internal + 3116
20 org.gnu.Emacs 0x000000010009e8be read_char + 2350
21 org.gnu.Emacs 0x00000001000a104f read_key_sequence + 1215
22 org.gnu.Emacs 0x00000001000a31f9 Fread_key_sequence + 313
23 org.gnu.Emacs 0x0000000100109256 Ffuncall + 1126
24 org.gnu.Emacs 0x0000000100145aae Fbyte_code + 6814
25 org.gnu.Emacs 0x0000000100108bfc funcall_lambda + 588
26 org.gnu.Emacs 0x0000000100109042 Ffuncall + 594
27 org.gnu.Emacs 0x0000000100145aae Fbyte_code + 6814
28 org.gnu.Emacs 0x0000000100108bfc funcall_lambda + 588
29 org.gnu.Emacs 0x0000000100109042 Ffuncall + 594
30 org.gnu.Emacs 0x000000010010a78e call1 + 30
31 org.gnu.Emacs 0x000000010009e44f read_char + 1215
32 org.gnu.Emacs 0x00000001000a104f read_key_sequence + 1215
33 org.gnu.Emacs 0x00000001000a35cb command_loop_1 + 587
34 org.gnu.Emacs 0x0000000100107717
internal_condition_case + 327
35 org.gnu.Emacs 0x000000010009a9a7 command_loop_2 + 55
36 org.gnu.Emacs 0x0000000100107820 internal_catch + 224
37 org.gnu.Emacs 0x000000010009b436 command_loop + 182
38 org.gnu.Emacs 0x000000010009b89f recursive_edit_1 + 159
39 org.gnu.Emacs 0x000000010009ba3f Frecursive_edit + 287
40 org.gnu.Emacs 0x000000010009102c main + 3452
41 org.gnu.Emacs 0x0000000100002034 start + 52
Thread 1: Dispatch queue: com.apple.libdispatch-manager
0 libSystem.B.dylib 0x00007fff801d512a kevent + 10
1 libSystem.B.dylib 0x00007fff801d6ffd _dispatch_mgr_invoke + 154
2 libSystem.B.dylib 0x00007fff801d6cd4
_dispatch_queue_invoke + 185
3 libSystem.B.dylib 0x00007fff801d67fe
_dispatch_worker_thread2 + 252
4 libSystem.B.dylib 0x00007fff801d6128 _pthread_wqthread + 353
5 libSystem.B.dylib 0x00007fff801d5fc5 start_wqthread + 13
Thread 0 crashed with X86 Thread State (64-bit):
rax: 0x0000000000000000 rbx: 0x0000000000000006 rcx:
0x00007fff5fbf3fe8 rdx: 0x0000000000000000
rdi: 0x000000000000f4af rsi: 0x0000000000000006 rbp:
0x00007fff5fbf4000 rsp: 0x00007fff5fbf3fe8
r8: 0x0000000000000001 r9: 0x0000000119ba57a0 r10:
0x00007fff80206616 r11: 0x0000000000000206
r12: 0x0000000000000006 r13: 0x0000000100534d48 r14:
0x0000000000000200 r15: 0x00000000000000ac
rip: 0x00007fff8020a5d6 rfl: 0x0000000000000206 cr2: 0x0000000102a35fff
Binary Images:
0x100000000 - 0x1001d9fff +org.gnu.Emacs Version 23.2
(9.0) <7D762A3A-B020-669B-93E9-CD4525AAB2E1>
/Applications/Isabelle2011.app/Contents/Resources/Emacs.app/Contents/MacOS/Emacs
0x1013aa000 - 0x1013aeff7 libFontRegistryUI.dylib ???
(???) <89E50DF0-2A72-B443-28AE-5F27EC7E22C7>
/System/Library/Frameworks/ApplicationServices.framework/Frameworks/ATS.framework/Resources/libFontRegistryUI.dylib
0x7fff5fc00000 - 0x7fff5fc3bdef dyld 132.1 (???)
<486E6C61-1197-CC7C-2197-82CE505102D7> /usr/lib/dyld
0x7fff800d1000 - 0x7fff801b7fef com.apple.DesktopServices
1.5.10 (1.5.10) <B7E00D85-F971-D85B-0217-482E15E9E924>
/System/Library/PrivateFrameworks/DesktopServicesPriv.framework/Versions/A/DesktopServicesPriv
0x7fff801b8000 - 0x7fff801bafff libRadiance.dylib ??? (???)
<73257486-8E94-E758-1A5A-5B521F27EE12>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/ImageIO.framework/Versions/A/Resources/libRadiance.dylib
0x7fff801bb000 - 0x7fff8037cfff libSystem.B.dylib 125.2.10
(compatibility 1.0.0) <9BAEB2F2-B485-6349-E1AB-637FE12EE770>
/usr/lib/libSystem.B.dylib
0x7fff803c1000 - 0x7fff804d8fef libxml2.2.dylib 10.3.0
(compatibility 10.0.0) <1B27AFDD-DF87-2009-170E-C129E1572E8B>
/usr/lib/libxml2.2.dylib
0x7fff80582000 - 0x7fff80740fff libicucore.A.dylib 40.0.0
(compatibility 1.0.0) <2C6ECACF-CD56-1714-6F63-CB6F5EE7A1E2>
/usr/lib/libicucore.A.dylib
0x7fff80741000 - 0x7fff80750fff com.apple.opengl 1.6.12
(1.6.12) <29482652-1E44-1C47-428F-1209AA65336D>
/System/Library/Frameworks/OpenGL.framework/Versions/A/OpenGL
0x7fff80751000 - 0x7fff80909fef com.apple.ImageIO.framework
3.0.4 (3.0.4) <EFB373AE-FE02-40C4-ABDC-09D61AFD25EA>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/ImageIO.framework/Versions/A/ImageIO
0x7fff8090a000 - 0x7fff80917fe7 libCSync.A.dylib 545.0.0
(compatibility 64.0.0) <45B5B514-7CEB-38A9-F34A-1D96F010EC42>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/CoreGraphics.framework/Versions/A/Resources/libCSync.A.dylib
0x7fff80918000 - 0x7fff8091dfff libGIF.dylib ??? (???)
<1B9DCB7F-CD1D-B23F-8AC6-5292B94A4D0E>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/ImageIO.framework/Versions/A/Resources/libGIF.dylib
0x7fff8091e000 - 0x7fff80cbbfe7 com.apple.QuartzCore 1.6.3
(227.36) <6FD8E129-135E-2F89-E9F0-A3CD0C6FCEF1>
/System/Library/Frameworks/QuartzCore.framework/Versions/A/QuartzCore
0x7fff80e1d000 - 0x7fff80ed3fff libobjc.A.dylib 227.0.0
(compatibility 1.0.0) <99CB3A0F-64CF-1D16-70CD-8AED2EF06C30>
/usr/lib/libobjc.A.dylib
0x7fff80fed000 - 0x7fff81018ff7 libxslt.1.dylib 3.24.0
(compatibility 3.0.0) <87A0B228-B24A-C426-C3FB-B40D7258DD49>
/usr/lib/libxslt.1.dylib
0x7fff8108e000 - 0x7fff81095fff com.apple.OpenDirectory 10.6
(10.6) <4200CFB0-DBA1-62B8-7C7C-91446D89551F>
/System/Library/Frameworks/OpenDirectory.framework/Versions/A/OpenDirectory
0x7fff81096000 - 0x7fff81130ff7
com.apple.ApplicationServices.ATS 4.4 (???)
<55B528A6-0C88-6CB8-152B-A34A440FACFE>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/ATS.framework/Versions/A/ATS
0x7fff81131000 - 0x7fff811b6ff7
com.apple.print.framework.PrintCore 6.3 (312.7)
<CDFE82DD-D811-A091-179F-6E76069B432D>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/PrintCore.framework/Versions/A/PrintCore
0x7fff81210000 - 0x7fff81214ff7 libCGXType.A.dylib 545.0.0
(compatibility 64.0.0) <49E6AF5D-AF9B-67CF-A6B8-C79F6BA8A627>
/System/Library/Frameworks/ApplicationServices.framework/Versions/A/Frameworks/CoreGraphics.framework/Versions/A/Resources/libCGXType.A.dylib
0x7fff81215000 - 0x7fff8132efef libGLProgrammability.dylib
??? (???) <C4BB281B-629D-08ED-2991-3D51671B0B02>
/System/Library/Frameworks/OpenGL.framework/Versions/A/Libraries/libGLProgrammability.dylib
0x7fff81348000 - 0x7fff8136dff7 com.apple.CoreVideo 1.6.2
(45.6) <E138C8E7-3CB6-55A9-0A2C-B73FE63EA288>
/System/Library/Frameworks/CoreVideo.framework/Versions/A/CoreVideo
0x7fff81873000 - 0x7fff81884ff7 libz.1.dylib 1.2.3
(compatibility 1.0.0) <97019C74-161A-3488-41EC-A6CA8738418C>
/usr/lib/lib
[message truncated]
Email Gateway (Aug 18 2022 at 17:37):From: Tobias Nipkow <nipkow@in.tum.de>
Use ~ for negation.
Tobias
Email Gateway (Aug 18 2022 at 17:37):From: Alexander Krauss <krauss@in.tum.de>
No idea about fixing the actual problem... but before it becomes a
show-stopper for you, you can fall back to ascii notation: "~ P" is the
same as "\<not> P".
Alex
Email Gateway (Aug 18 2022 at 17:37):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I had the same problem. It seems as if the Unicode-Token/X-Symbol Syntax
with \<...> is causing it. There is however the alternative to use just
\... (which works in most cases) and which doesn't cause the same
problem. Hence, if you would like to have nice symbols, I recommend to
enter \not for negation (which will expand to \<not> but -- at least on
my machine (and I'm on Fedora Linux) -- doesn't lead to a crash).
cheers
chris
Email Gateway (Aug 18 2022 at 17:38):From: David Aspinall <David.Aspinall@ed.ac.uk>
That's really nasty! I can reproduce on Linux. It seems to happen when
you type near the end of the buffer: if there is a good amount of text
or whitespace after the token you're typing it works OK.
It seems to be a similar case to this one:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/318
which happens when you type \<module> almost anywhere.
I'll try escalating this low-level bug with the Emacs developers.
- David
Last updated: Apr 18 2024 at 16:19 UTC