Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-06-30

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

All times shown according to UTC.

Time Nick Message
01:53 fracting joined #isabelle
02:28 fracting joined #isabelle
04:32 fracting joined #isabelle
07:48 larsrh_ joined #isabelle
09:31 fracting joined #isabelle
09:50 fracting joined #isabelle
11:24 silver joined #isabelle
11:46 dmiles joined #isabelle
14:33 fracting joined #isabelle
15:20 fracting joined #isabelle
17:12 fracting joined #isabelle
18:53 popinman322 Was sledgehammer support for Alt-Ergo removed or did it never exist in the first place? :o
18:55 popinman322 ... or how do I use it?
19:00 popinman322 Dash to underscore. Of course. :|
22:08 larsrh popinman322: I only found a NEWS entry noting its addition
22:08 larsrh Did you try it and it didn't work?
22:15 popinman322 larsrh, it didn't work initially, I had to edit "src/HOL/Tools/ATP/atp_systems.ML"
22:16 popinman322 My `why3` required an additional command line parameter (the initial "prove" command)
22:16 popinman322 My initial comment was just because I tried "alt-ergo" instead of "alt_ergo"
22:16 larsrh In that case probably something changed in why3
22:16 larsrh I'd recommend posting this on the mailing list
22:17 larsrh I don't think many people use alt-ergo with sledgehammer
22:17 popinman322 I mean, I just added it on a whim... I just happened to have it on my system so "why not?"
22:18 popinman322 Is there a reason people don't use alt-ergo with sledgehammer?
22:19 popinman322 larsrh, Should I drop this by the dev list?
22:21 larsrh popinman322: no, regular isabelle-user
22:21 larsrh popinman322: the reason being "it's not default", I suppose
22:29 Damaki joined #isabelle

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