# IRC log for #isabelle, 2017-07-01

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01: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/
08:15 pruvisto chindy: locale foo_eucl = foo a for "a :: euclidean_space"
08:15 pruvisto something like that
08:15 pruvisto er
08:15 pruvisto for a :: "'a :: euclidean_space"
08:15 pruvisto then anything defined/proven in foo will be available in foo_eucl
08:15 pruvisto since foo_eucl is a sublocale of foo
08:19 int-e http://downthetypehole.de/paste/Hg7Q66YW is a toy example covering, I think, the basics of locales.
08:31 int-e But of course you should also look at the locales tutorial (see the document panel)!
08:38 dmiles joined #isabelle
11:26 chindy oh wow.. thats a great min example thanks
14:57 larsrh heh, there's a thread on [hol-info] right now that could be solved by "use fsets" :-)
18:02 larsrh 20:01 <larsrh> !term λx. x
18:02 larsrh 20:01 <isabelle-bot> λx. x :: 'a ⇒ 'a
18:02 larsrh soon in an #isabelle near you
18:17 larsrh 20:16 <larsrh> !value 3 + 4 :: nat
18:17 larsrh 20:16 <isabelle-bot> Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))
18:19 larsrh those two ought to be enough for now
18:44 pruvisto haha
18:45 pruvisto !import Probability
18:45 larsrh don't laugh, I'm deploying this right now
18:45 pruvisto !import Flyspeck-Tame
18:45 larsrh you wish
18:45 pruvisto I'm not satisfied until I can do entire proofs on IRC :P
18:48 larsrh PRs welcome: https://github.com/larsrh/isabelle-irc-bot
18:55 larsrh anyway, you'll get Complex_Main
18:55 larsrh building HOL on two cores is slooooow
19:10 isabelle-bot joined #isabelle
19:10 larsrh !test hi
19:10 isabelle-bot larsrh: hi
19:10 larsrh !value 3 + 4 :: nat
19:10 isabelle-bot larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))
19:10 larsrh have fun
19:11 larsrh better dial down the log level a notch
19:11 isabelle-bot joined #isabelle
19:12 larsrh !value 3 + 4 :: nat
19:12 isabelle-bot larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))
19:12 larsrh that's better
19:13 larsrh you can use !value and !term, those correspond to the commands in Isabelle
19:15 larsrh oh, and it also responds to /query
19:17 pruvisto larsrh: does it have some kind of timeout?
19:18 larsrh no, not really
19:18 larsrh but it is possible to run multiple things at the same time
19:18 larsrh !value 20 * 20 :: nat
19:18 larsrh !value 20 * 20 :: nat
19:18 isabelle-bot larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
19:18 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:18 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:18 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:18 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
19:18 isabelle-bot larsrh: Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
19:19 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:19 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:19 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (S
19:19 isabelle-bot (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
19:19 larsrh oops, that might have been a little bit too large
19:19 pruvisto !value remdups_adj (filter (%x. x \<noteq> 0) [1,0,1,1,-1,0,-1,0,1,1,0::nat]))
19:19 isabelle-bot pruvisto: Could not read term
19:19 pruvisto !value remdups_adj (filter (%x. x \<noteq> 0) [1,0,1,1,-1,0,-1,0,1,1,0::nat])
19:19 isabelle-bot pruvisto: [1, - 1, 1]
19:20 pruvisto and, yeah, frankly, I think some kind of timeout and flooding protection might be good
19:20 larsrh !term -1::nat
19:20 isabelle-bot larsrh: Could not read term
19:20 larsrh pruvisto: yeah, possibly
19:22 pruvisto :term (-1)::nat
19:22 pruvisto !term (-1)::nat
19:22 isabelle-bot pruvisto: Could not read term
19:23 larsrh okay, so default flood protection seems to be that all outgoing messages are spaced at least 1s apart
19:23 larsrh I could increase that
19:24 larsrh ah, turns out the -1 :: nat thing uses coercions ^^
19:26 pruvisto larsrh: a common approach is also something like "response would have more than 5 lines; you have to use /query for that"
19:27 pruvisto to avoid polluting the public channels
19:27 larsrh right
19:27 pruvisto but nice to have this, thansk!
19:27 pruvisto *thanks
19:28 larsrh as I said, it's on GitHub :p
19:28 int-e aaaaaargh
19:28 int-e isabelle-bot: what are you ;-)
19:28 pruvisto !term filterlim (λx. x^2) at_top sequentially
19:28 isabelle-bot pruvisto: filterlim power2 sequentially sequentially :: bool
19:28 pruvisto !term filterlim (λx. x^3) at_top sequentially
19:28 isabelle-bot pruvisto: LIM x sequentially. x ^ 3 :> sequentially :: bool
19:29 larsrh !test int-e: I'm the new bot ^.^
19:29 isabelle-bot larsrh: int-e: I'm the new bot ^.^
19:29 pruvisto That… is not what I expected.
19:29 pruvisto Oh well.
19:29 larsrh pruvisto: what did you expect?
19:29 pruvisto different syntax
19:30 int-e larsrh: apparently, adding a smiley and not adding a question mark does not save one from answers to rhetorical questions.
19:30 larsrh this is literally what comes out when you call "Syntax.string_of_term o Syntax.read_term"
19:30 pruvisto ah no
19:30 pruvisto !term filterlim (λx. x^3) (nhds 10) sequentially
19:30 isabelle-bot pruvisto: (λx. x ^ 3) ⇢ 10 :: bool
19:31 pruvisto yup
19:31 pruvisto !term filterlim (λx. x^3) (nhds 10) (at 3)
19:31 isabelle-bot pruvisto: (λx. x ^ 3) ─3→ 10 :: bool
19:31 larsrh nice arrow
19:31 pruvisto that's more like it
19:31 pruvisto although that's virtually unreadable on a fixed-width character terminal
19:31 int-e I hope there's a sane limit on the length of its output.
19:31 * larsrh whistles
19:31 lambdabot joined #isabelle
19:31 int-e > [1..]
19:31 lambdabot [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,...
19:32 int-e that's comparatively short, admittedly.
19:32 lambdabot left #isabelle
19:32 pruvisto I wonder if it supports codatatypes :P
19:32 int-e (lambdabot is more verbose in private chat)
19:33 pruvisto Unfortunately, "Stream" isn't part of Complex_Main
19:33 larsrh didn't know you could make lambdabot join other channels
19:33 larsrh fine, I'll implement limits.
19:33 int-e Hmm, I'm actually the one hosting it... so yes I can.
19:33 larsrh heh
19:34 pruvisto int-e: oh, nice. I did not know that.
19:34 larsrh The Botfather
19:34 pruvisto larsrh: so, is this your response to Makarius' VSCode backend?
19:34 int-e Well I took over maybe 5 years ago... it was dons, then Cale, then mokus0 I guess, then me? There may be gaps in my memory.
19:34 pruvisto Isabelle/IRC – at least as usable as VSCode
19:35 pruvisto (and with much less memory consumption, and no JavaScript)
19:41 pruvisto larsrh: I was expecting you to do some kind of joke like "You want me to implement limits? Isn't that /your/ job?"
19:51 larsrh can't make jokes, busy hacking
20:35 larsrh will rejoin tomorrow
20:45 ilbot3 joined #isabelle
20:45 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/