Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-14

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 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/
10:55 silver joined #isabelle
13:42 JCaesar Hm. Time to try this again. I've got some isabelle definition that produces a list of strings. I'd like to write those strings, one per line, to a file, using ML.
13:43 JCaesar I can use Code_evaluation.dynamic_value to evaluate the definition. But then I still have some isabelle term, and not a list of ML strings…
13:43 JCaesar is there a way to go between the two?
13:44 larsrh after that use HOLogic.dest_list
13:44 larsrh then use HOLogic.dest_string
13:51 JCaesar larsrh: ty. Seems to work.
18:07 chindy when sledgehammer returns multiple proofs including an isar proof is there any preferencial way of selecting wich one to use?
18:40 stoopkid joined #isabelle
19:35 JCaesar chindy: As long as you're not working on something you want to publish: either take whatever runs shortest or is the shortest to scroll over, whichever you prefer.
19:36 JCaesar I've had one or the other rare case where the isar proof did actually contain some reasonably readable and interesting fact. but mostly, the level of insight and intuition that either of the two proof types provide is low, so it doesn't matter much.
19:38 JCaesar Isar proofs might be a bit more laborious to fix, in case of an Isabelle update, but they might also be easier to fix in case the proof can't be found by sledgehammer anymore…
19:38 JCaesar In the end… I don't think there is a strong preference towards either, but I'm no authority on this.
21:26 int-e wee, that was a scary error. http://sprunge.us/LiLE ... (The key is, "No X11 DISPLAY variable was set"... it simply was the wrong shell.)
21:35 pruvisto Yeah I've had errors like this
21:36 pruvisto and the cause was usually that I'd been working in an SSH session on a computer several kilometres away without noticing for half an hour
22:30 chindy JCaesar: so what would you do if you would want to publish something?
22:31 JCaesar if the one-line proof isn't too unreasonable, use that. otherwise, write my own isar proof…
23:53 ertes joined #isabelle

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