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 
inte 
http://downthetypehole.de/paste/Hg7Q66YW is a toy example covering, I think, the basics of locales. 
08:31 
inte 
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 [holinfo] right now that could be solved by "use fsets" :) 
18:02 
larsrh 
20:01 <larsrh> !term λx. x 
18:02 
larsrh 
20:01 <isabellebot> λ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 <isabellebot> 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 FlyspeckTame 
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/isabelleircbot 
18:55 
larsrh 
anyway, you'll get Complex_Main 
18:55 
larsrh 
building HOL on two cores is slooooow 
19:10 

isabellebot joined #isabelle 
19:10 
larsrh 
!test hi 
19:10 
isabellebot 
larsrh: hi 
19:10 
larsrh 
!value 3 + 4 :: nat 
19:10 
isabellebot 
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 

isabellebot joined #isabelle 
19:12 
larsrh 
!value 3 + 4 :: nat 
19:12 
isabellebot 
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 
isabellebot 
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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
19:18 
isabellebot 
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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (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 
isabellebot 
(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 
isabellebot 
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 
isabellebot 
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 
isabellebot 
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 
isabellebot 
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 
inte 
aaaaaargh 
19:28 
inte 
isabellebot: what are you ;) 
19:28 
pruvisto 
!term filterlim (λx. x^2) at_top sequentially 
19:28 
isabellebot 
pruvisto: filterlim power2 sequentially sequentially :: bool 
19:28 
pruvisto 
!term filterlim (λx. x^3) at_top sequentially 
19:28 
isabellebot 
pruvisto: LIM x sequentially. x ^ 3 :> sequentially :: bool 
19:29 
larsrh 
!test inte: I'm the new bot ^.^ 
19:29 
isabellebot 
larsrh: inte: 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 
inte 
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 
isabellebot 
pruvisto: (λx. x ^ 3) ⇢ 10 :: bool 
19:31 
pruvisto 
yup 
19:31 
pruvisto 
!term filterlim (λx. x^3) (nhds 10) (at 3) 
19:31 
isabellebot 
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 fixedwidth character terminal 
19:31 
inte 
I hope there's a sane limit on the length of its output. 
19:31 
* larsrh 
whistles 
19:31 

lambdabot joined #isabelle 
19:31 
inte 
> [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 
inte 
that's comparatively short, admittedly. 
19:32 

lambdabot left #isabelle 
19:32 
pruvisto 
I wonder if it supports codatatypes :P 
19:32 
inte 
(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 
inte 
Hmm, I'm actually the one hosting it... so yes I can. 
19:33 
larsrh 
heh 
19:34 
pruvisto 
inte: 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 
inte 
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/ 