Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-21

| 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/
03:09 newbie joined #isabelle
03:16 newbie|4 joined #isabelle
03:19 IsM joined #isabelle
03:23 IsM Good thing I don't need help with IRC. I guess I'd figure it out eventually. I'm just here warming up for the diss.
03:23 IsM For tomorrow?
03:24 IsM It is tomorrow. 3:23 London time. 9:24PM Central time.
03:32 IsM I put forth a book as a decent test on whether a particular person can actually do abstract algebra in Isabelle HOL. Notice that I say "particular person". The software is capable, but the AFP posers are lacking. Am I lacking. Of course, but I'm not an AFP poser.
03:32 IsM Abstract Algebra, 3rd, by Dummit and Foote.
03:33 IsM http://www.amazon.com/Abstract-Algebra-3rd-David-Dummit/dp/0471433349
03:34 IsM This would be advanced undergrad, or masters level. It has good coverage, but not so advanced as Lang, not that I'm any authority on algebra.
03:35 IsM Are the AFP posers ready for the diss?
03:39 IsM The diss is the challenge. It's a fact. Even though the AFP posers are the experts, they would be shut down on that book, very quickly. Something they need would be missing, in what I'll call the HOL infrastructure. The theory may be abstract, but it's mixed in a lot with the concrete. But hey, prove me wrong, but you don't get to pick and choose. You start at the beginning, and do it all. Okay, I
03:42 IsM It's not my problem anymore. Logic don't pay the bills anyway. I'm not saying the AFP posers aren't nice, helpful people. Some of them are extraordinarily helpful.
03:44 IsM I guess all of it is too demanding. You can cut out 10% of it. C'mon, you can't do it, and that's the diss.
04:00 spacekitteh how do i do the equivalent of haskell's [1,2,...]?
04:00 spacekitteh er [0,1,2,...] as in the list of nats
05:58 spacekitteh nevermind
05:59 spacekitteh is there a lookup function?
05:59 spacekitteh i.e. a "'a list => 'a => nat option"
06:56 ThreeOfEight spacekitteh: you can write a /stream/ of natural numbers
06:56 ThreeOfEight but not a list
06:56 ThreeOfEight because lists have finite length
06:56 spacekitteh yeah it's k i figured out a better way
06:56 ThreeOfEight lazy lists can be finite or infinite; streams are always infinite
06:57 ThreeOfEight spacekitteh: http://afp.sourceforge.net/entries/List-Index.shtml
06:57 ThreeOfEight this is the AFP entry I mentioned
06:58 ThreeOfEight it does not return an option, unfortunately
06:59 ThreeOfEight if you really need an option, you can either adapt that function or put your own function on top of it so you can re-use some of its lemmas, I guess
07:03 spacekitteh yeah.
07:05 ThreeOfEight in fact, if you do something like that, it might make a good addition to said AFP entry
12:22 IsM joined #isabelle
12:41 IsM IRC is much more to my liking, than a domain owned by Cambridge, though I suppose a person has to behave themselves here some also, since a channel is owned.
12:42 IsM I assume that 'larsrh', who has posted here, is the same person who has told me "Do not contact me privately, ever again. Your AFP criticism is ludicrous."
12:42 IsM There are several things to say about that.
12:42 IsM (1) First and foremost is that larsrh is another person who has a fundamental misunderstanding of what the Internet is. People at the top seem to think they're special, so special that they have the right to command the world on how to use email.
12:42 IsM (2) It was a one-shot deal, dude. You're acting as though I wanted to have a conversation with you, by email. You're actually rather low on the totem pole, within that group.
12:42 IsM (3) In fact, part of my rule to generally not email "special people" is because, to them, everybody's a terrorist who's not on their side.
12:42 IsM (4) You don't own the Internet, larsrh. I'll send you an email any time I want to. It happens to be, I don't want to. Again, at this point, you're rather low. But I don't even email the top dogs. But you have hear of filters, haven't you? You do work with computers, don't you, larsrh?
12:42 IsM (5) Did I miss that part that you're rather low on the totem pole. You got "blessed" because of other important people it was sent to. It wasn't about you, execpt maybe as an AFP poser.
12:42 IsM (6) Well, it turns out that I have met your command. This is public, is it not?
12:43 larsrh IsM: You are posting content of private communication. This is illegal in many jurisdictions.
12:46 IsM I've learned the ways of IRC. That's okay. It's a free for all. There are other things to do in life.
12:55 larsrh For context: IsM sent a long and rambling mail to the mailing list (not gone through yet) and a couple of Isabelle users privately, containing random accusations. I told him off.
13:15 Mr_Reject joined #isabelle
13:16 Mr_Reject Gettin' educated on the decorum of IRC. That's a good thing. Control is not a bad thing. Better to work than engage in diss on someone else's domain. I wouldn't know what the law is, but a wise person shouldn't expect that privacy of emails will be respected. I don't. And I explicitly stated it wasn't a private correspondence.
13:16 Mr_Reject Adios. It's your domain, obviously, not mine. I'll make sure I save all this to be able to show I haven't been a terrorist. Being but a momentary vapor on IRC is all good.
13:20 Mr_Reject I was totally confused. Looking at the day before, trying to sync up my IRC client with what's on the web. Anyway, Isabelle is a great product. There's no reason for me to be here.
13:23 Mr_Reject On the other hand, now that I'm not confused, and it appears I haven't gotten banned, I can be tempted: work or diss. Surely the choice should be work.
13:35 JCaesar larsrh: For future reference… who has op here?
13:38 larsrh JCaesar: Igloo and lispy, judging by /msg ChanServ access #isabelle list
13:38 JCaesar Oh, right, ChanServ can do that…
16:03 JCaesar So how do I get Isabelle to build me a proof document? isabelle build -v -o document=pdf -d . BDDs doesn't seem to work. (I've got a root file saying session "BDDs" = …)
16:11 ThreeOfEight JCaesar: define "does not work"
16:11 ThreeOfEight is there any output regarding the document file?
16:11 ThreeOfEight also, do you have a document directory with a root.tex?
16:12 JCaesar no, and no.
16:13 ThreeOfEight yes, you should get one
16:13 ThreeOfEight I think isabelle mkroot actually makes one
16:13 ThreeOfEight alternatively, you can just take one from the AFP as a template
16:13 larsrh $ isabelle mk
16:13 larsrh $ isabelle mkroot -d
16:14 ThreeOfEight larsrh: does that work when there already is a ROOT file?
16:15 larsrh no
16:15 JCaesar Figures…
16:15 larsrh you can run it in an empty directory and pull out the 'document' folder
16:38 JCaesar Got it, thank you.
17:22 newbie|4 joined #isabelle
17:25 newbie|4 I'm not newbie4, but I don't want to change it. Thank larsrh for the possibility of the Streisand effect, if that be the case.
17:25 newbie|4 Let the search engines find it or not: "An Open Dissfest to the Isabelle/HOL AFP Posers (with small Luddite Mathematicians tangent)". Read it or ignore it. Either way, it's all good.
17:26 newbie|4 https://gist.github.com/GezzMC/6d4a0a6d72886e14f9ba
17:26 newbie|4 I'm not out to hijack this channel. Some people need a lesson in what the web is about. To retain freedom, we need to exercise freedom.
17:26 newbie|4 Thanks to the channel owners who set this up. The points about the abstract algebra book are valid. It's ridiculous when the posers can't cover a standard algebra book.
17:29 newbie|4 Lucky you. I'm using a VPN, and it seems Gist thinks I'm a robot, and has hidden my account. Oh well.  Maybe so, or maybe not.
17:30 larsrh Is it me or does GB not make any sense at all?
17:30 int-e It's not just you.
17:32 larsrh His latest rant still hasn't made its way to the mailing list; I'm assuming Larry deleted it.
17:33 larsrh (for good reason)
17:37 int-e Dang, now I'm kind of curious what he wrote. Not that I would get very far in reading it... it's hard to follow a random walk.
17:42 larsrh He called the AFP "stupid", AFP contributors "posers" and "pretenders", and Andrew Wiles a "mathematical-credit-stealer".
17:45 larsrh I'd laugh if it weren't so hostile.
18:10 IsM joined #isabelle
18:17 IsM I've been there and done that with rhetorical combat. It's not a challenge if I'm not out numbered. At the I'm-just-a-whipping-boy point, it's time to pull out. The channel owners are free to speak up and declare the rules.
18:18 IsM The lesson is, leave Gist and GitHub for your serious work. Find a blog for your flames. In the Gist, I did argue from the point that I'm insane and ramble 90% of time.
18:18 IsM I present myself as knowing nothing. C'mon Lars, what did you not get about  you not being able to do undergrad level abstract algebra? You guys are the experts. You pick and choose to make it look like you can do something.
18:34 IsM Larry is the moderator. It's his job to delete stuff like that. In the gist, I noted how in the past, I sent a flame to the mailing list, but with "BLOCK THIS:..." in the title, at a time when my emails normally went through. You're best friends with Larry, ask him to verify it.
18:34 IsM Checking out for today. Apologies to those I would apologize if I knew you well enough.
18:48 lispy Not sure I banned the right person there
18:49 lispy larsrh, JCaesar: Do you know which nick corresponds to the mailing list traffic?
18:50 lispy certainly, IsM sounds trollish though.
21:06 tautologico what was that?
21:34 larsrh lispy: IsM == newbie|4 == Mr_Reject == Gottfried Barrow on the mailing lists
21:44 lispy larsrh: thanks
22:50 ThreeOfEight I find this amusing and upsetting at the same time.
22:52 ThreeOfEight For the record, we actually do have a part of the abstract algebra he mentioned formalised already, and the main reason why we don't have more is because the Isabelle internals make doing these things a bit tedious
22:52 ThreeOfEight /and/ because the Coq people already have a lot of algebra and if you formalise stuff that already exists in another system, people are generally not very impressed
22:53 ThreeOfEight regardless, I considered formalising some of it in my spare time at some point, and just today I had a student in my office who was interested in formalising Galois theory

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