Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-09-02

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

All times shown according to UTC.

Time Nick Message
00:38 pruvisto joined #isabelle
01:52 ilbot3 joined #isabelle
01:52 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/
03:43 hazyPurple joined #isabelle
05:02 hazyPurple joined #isabelle
06:01 hazyPurple joined #isabelle
06:15 hazyPurple joined #isabelle
06:17 hazyPurple joined #isabelle
06:19 hazyPurple joined #isabelle
06:38 hazyPurple joined #isabelle
08:09 numee joined #isabelle
13:57 hazyPurple joined #isabelle
14:50 chindy how do you guys generate snippets? the way i do it leads to problems when generating a proof document (using "
14:50 chindy text_raw {*\DefineSnippet{snippetXS}{*}").
14:59 int-e The way I've seen it, one has a separate leaf theory file for generating the snippets, and a separate session for building the snippet file.
15:01 int-e So it's not part of the theory development at all, and thus doesn't interfere with proof document generation. I have not seen any attempts of combining the two. (For proofs, one can take a finished proof and copy it to the snippet file. It's not nice to have this duplication, but it's the best way I know.)
16:50 pruvisto I never do that at all
16:50 pruvisto I always typeset all of my LaTeX by hand
16:50 pruvisto I find that Isabelle-generated LaTeX awful
20:00 hazyPurple joined #isabelle
20:01 hazyPurple joined #isabelle

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