Camelia, the Perl 6 bug

IRC log for #isabelle, 2012-01-18

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
05:51 eyebloom joined #isabelle
07:17 eyebloom joined #isabelle
16:00 eyebloom joined #isabelle
16:18 phimuemue_ joined #isabelle
16:58 eyebloom joined #isabelle
18:06 eyebloom joined #isabelle
19:10 eyebloom joined #isabelle
21:49 davidL anyone here have issues using the \<foo> symbols? isabelle/emacs (64-bit) crashes whenever I try entering one of those names with the following error: Fatal error (6)Aborted
21:53 int-e no. I had font troubles, but no crashes.
21:56 davidL strange
21:57 int-e (6) sounds like a failed assertion somewhere (it's usually a call to abort() and assert() is then the first suspect for calling that) -- is there any debug output before the crash?
21:57 davidL nope
21:57 davidL $ ./bin/isabelle emacs
21:57 davidL Fatal error (6)Aborted
22:04 larsrh strace?
22:04 larsrh $ strace ./bin/isabelle emacs
22:09 int-e Ok, the  Fatal error (6)  nessage is probably printed by a signal handler inside emacs (I checked, there is code for that), the 'Aborted' by the shell itself.
22:09 davidL here is some of the strace output (right before it crashes): http://paste.lisp.org/display/127155
22:11 int-e ohwow, emacs contains a lot of calls to abort() without any useful messages :/
22:13 int-e gotta run, I'd either play with gdb or try to find a different emacs version to play with.
22:14 davidL I'll email the users list as well; maybe someone else has run into this :)
22:14 davidL thanks a bunch
23:05 dschoepe joined #isabelle
23:08 dschoepe Is there a way to force isabelle to accept a function for which it can't prove termination, besides activating Skip Proofs in the menu? (I need this for a course where we only use isabelle for specification anyway)
23:36 larsrh dschoepe: how about using an inductive instead?
23:38 dschoepe larsrh: Would that still allow me to work with the object as if it was a function?
23:38 larsrh dschoepe: it really depends on your proofs
23:39 larsrh you might have to generate elimination rules with inductive_cases
23:39 dschoepe Sadly, we don't do any proofs at all in that course.
23:39 larsrh in my experience (advanced beginner) it works quite well
23:40 larsrh What do you do then?
23:40 larsrh are you going to generate code from the specification?
23:40 dschoepe Just specifying relations and stating properties about them, etc.
23:40 larsrh I think you should be fine with an inductive then
23:41 dschoepe No, we just use Isabelle to have a syntax-checked language for formal specification. We won't do anything with the results.
23:41 dschoepe Thanks, I'll try.

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary