Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-25

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

All times shown according to UTC.

Time Nick Message
03:02 wagle joined #isabelle
05:59 hazyPurple joined #isabelle
07:58 chindy what does that mean:  Exception trace - exception UNDEF raised (line 524 of "Isar/toplevel.ML")
07:58 chindy or rather do I need to fix this ?
08:00 larsrh it's an internal error that in the general case should not surface to the user
08:00 dave24 joined #isabelle
08:01 larsrh we'd need to see the code snippet that exhibits the error
08:37 chindy Thing is i dont know, it appears in every proof mode
08:46 larsrh Even if you start an empty file and just import Main?
08:47 chindy then i have Exception trace - exception UNDEF raised (line 450 of "Isar/toplevel.ML")
08:47 chindy Exception trace - exception UNDEF raised (line 409 of "Isar/toplevel.ML")
08:47 chindy Exception trace - exception UNDEF raised (line 390 of "Isar/toplevel.ML")
08:50 larsrh are you on Isabelle2016-1 or devel?
08:50 chindy 2016-1
08:51 larsrh o.O
08:51 larsrh I suggest nuking $HOME/.isabelle for starters
08:51 chindy but i might have "broken" my installation yesterday anyways
08:51 larsrh most likely cause is that some bit is flipped in the wrong way somewhere
08:52 larsrh ah, I haven't read yesterday's discussion here
08:52 chindy :)
08:52 larsrh yeah, the 64 bit story in Isabelle is a story of ignoring user needs
08:53 larsrh sadly
08:53 larsrh here's the excerpt from the etc/settings in the CI setup:
08:54 larsrh ML_OPTIONS="-H 4000 --maxheap 8G"
08:54 larsrh ML_PLATFORM="$ISABELLE_PLATFORM64"
08:54 larsrh ML_HOME="$POLYML_HOME/$ML_PLATFORM"
10:20 pruvisto larsrh: so what about that option in jEdit?
10:20 pruvisto the "ML System 64"?
10:20 larsrh I have no idea
10:20 larsrh I wasn't even aware that options influence bootstrapping
12:51 hazyPurple joined #isabelle
15:15 hazyPurple joined #isabelle
15:19 int-e can I force application of simp rules inside an if?
15:21 int-e ah, apply (simp cong del: if_weak_cong)
15:22 int-e ref: http://stackoverflow.com/questions/15627676/why-wont-isabelle-simplify-the-body-of-my-if-then-else-construct
15:53 hazyPurple joined #isabelle
16:22 ezyang joined #isabelle
16:28 hazyPurple joined #isabelle
17:24 hazyPurple joined #isabelle
19:24 JCaesar Kinda weird that deleting a cong rule would allow more simplifications to take place…
19:52 int-e well, the default `if` cong rule is weaker than the function cong rule; this is useful when the conditional guards a recursive call in a function definition
20:38 chindy Is the matryoshka project already part of the default isablle?
20:59 ertesx joined #isabelle

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