Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-01-28

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
14:42 chuchucorny int-e: thx :)
17:28 JCaesar Hm, I had a funny idea… what if there was a tool, let's call it autohammer, that would, as long as there is still a subgoal, invoke sledgehammer/try, take the best proof (maybe some balance between speed and length?), inserst it, but don't delete itself. If there's no subgoal left, it just does nothing. Additionally, if the command is used multiple times, the ones further down in the file have to wait
17:29 JCaesar for the ones further up to terminate.
17:29 JCaesar Now, further, what if the "proof outline with cases" would insert autohammer at the subcases?
17:30 JCaesar (as a bonus, if there are only isar proofs with timeout subgoals, it could sorry those out and itsert itself there.)
17:35 pruvisto I don't think that would be very useful for the kinds of things I tend to work on
17:36 pruvisto but I am somewhat reminded of that "try_hard" command
17:36 pruvisto I think Yukata from Data61 worked on that
17:48 JCaesar The things I'm doing right now has tons of that. Essentially, after you apply the right induction rule, sledgehammer can take care of the rest.
17:49 JCaesar Stuff also often has 10+ subgoals, so I'd like to just place sledgehammer, get a coffee, and come back to "proof done".
17:57 pruvisto sounds like maybe you really do want to try try_harder
17:58 pruvisto see https://github.com/data61/PSL
17:59 pruvisto Yutaka Nagashima, that was his name
18:33 JCaesar Guess I do want to have a look at it.
19:13 larsrh I need to send him a PR so that this project can be used simply with libisabelle :-)

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