Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-02-04

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

All times shown according to UTC.

Time Nick Message
04:13 tangentstorm joined #isabelle
04:17 tautologico joined #isabelle
04:19 ThreeOfEight joined #isabelle
04:20 Guest98671 joined #isabelle
17:29 JCaesar "by moura" ?¿?
17:31 JCaesar "solves skolemization goals." Hmm. Nevermind my surprize, everything is explained.
17:42 larsrh JCaesar: presumably named after de Moura, one of the major developers of Z3
20:46 tautologico_ joined #isabelle
21:42 JCaesar I've never actually tried code generation. Is there a tutorial of stuff I should know about? (I ran into https://bpaste.net/show/e493501fad2d , which is why I'm asking.)
21:45 spacekitteh-work oh god i have to try to figure out how to change sledgehammer ML arrays to work operate in parallel
21:51 spacekitteh-work hold me i'm scared
21:53 larsrh spacekitteh-work: Not sure what you mean. Sledgehammer tries provers in parallel.
21:53 larsrh JCaesar: That should actually be explained in the manual :-)
21:54 larsrh JCaesar: try this: export_code foobar in Haskell module_name Conc_Impl file Conc_Impl.hs
21:54 spacekitteh-work larsrh: i'm talking about MaSh
21:55 spacekitteh-work specifically, its learning algorithm
21:55 spacekitteh-work it's single threaded
21:55 spacekitteh-work and trying to learn from ~50,000 facts single-threadedly takes like, 70 hours
21:56 larsrh spacekitteh-work: wow, that's a lot
21:56 spacekitteh-work facts or hours?
21:56 larsrh You can disable MaSh if you don't need it
21:56 spacekitteh-work i want mash though, so we can actually use sledgehammer
21:56 spacekitteh-work without it it's useless for our codebase
21:56 larsrh Understood.
21:56 larsrh I think it'd be best to ask Jasmin what can be done there
21:57 spacekitteh-work it looks like it does a manual for loop over each of the elements of the facts array
21:57 spacekitteh-work and i'm trying to figure out if it's safe to parallelise because it -looks- embarassingly parallel
21:59 spacekitteh-work is she on irc?
21:59 larsrh No, don't think so.
21:59 larsrh BTW, Jasmin is male :-)
21:59 spacekitteh-work oh
21:59 larsrh spacekitteh-work: In what part of the code is that loop?
22:05 spacekitteh-work sledgehammer_mash.ml
22:05 spacekitteh-work learn_facts
22:05 spacekitteh-work line 321
22:08 larsrh Hmm, hard to say. A lot of imperative updating going on
22:09 spacekitteh-work yeah :\
22:11 spacekitteh-work i *think* it could be adapted

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