Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-01-14

| 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/
11:25 silver joined #isabelle
11:35 silver_ joined #isabelle
11:57 JCaesar hm, I complained that using sledgehammer would occupy a few gb of disk space once in a while, right? I just noticed that cvc4 likes (or liked, with Isabelle2016) to crash. And systemd collects coredumps. Maybe it's that…
11:58 JCaesar anyway, just deleted a few GB of core dumps… (total coredumpd use is limited to 4 by default, but that's still ridiculous.)
12:38 int-e larsrh: I've just found HOLF, and I'm really excited about it! This should make all my future Isabelle developments a breeze. I'm just wondering why there are so few users of this logic. Perhaps all that's missing is an update to Isabelle 2017? (found via http://inutile.club/estatis/falso/ )
12:52 larsrh int-e: Pull Request welcome :-) https://github.com/fu-dietersheim/hol-falso
12:53 larsrh BTW, there's also Isabelle/LOL if you're looking for something even simpler https://github.com/fu-dietersheim/isabelle-lol
15:12 ammbauer joined #isabelle
16:24 JCaesar that example file should have been named ontolology.
16:49 JCaesar Hm, putting . in a ROOTS file causes a *** java.lang.StackOverflowError when invoking build.
18:54 JCaesar What do I have to do to use mathpartir? put the sty file in my document folder, \usepackage, anything else? I want thm[mode=Rule] to work…
19:20 chindy joined #isabelle
21:38 AtnNn Hi, I'm working through the Programming and Proving tutorial. How can I pattern match on the int 0?
21:40 larsrh AtnNn: I don't think you can, unfortunately

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