Log of the #nice channel on irc.freenode.net

Using timezone: Central European Time
* ChanServ leaves01:00
* arjanb leaves
* CIA-2 leaves
* falconair leaves
* DRMacIver leaves
* falconair leaves01:35
* falconair joins06:12
* bonniot joins09:48
* bonniot leaves11:01
* bonniot joins
* bonniot leaves11:11
* DRMacIver leaves
* CIA-2 leaves
* bonniot joins12:00
* CIA-2 joins
* DRMacIver joins
* falconair leaves13:18
* ArtemGr joins15:07
* ArtemGr leaves15:11
* arjanb joins16:54
Nice assertions obviously don't behave like I thought they did...
<bonniot>in what way?18:10
<DRMacIver>Well for starters I just wrote a trivial test which began the main method with 'assert(0 > 1)' and the method appears to run without a hitch. :)18:12
<bonniot>you know how to turn assertions on in your jvm?
it's off by default18:13
<DRMacIver>Yes, I'm assuming that's the problem.
<bonniot>java -ea ...
<DRMacIver>But I thought for some reasons Nice assertions were configured to always be on.
Good to find that out now. :)18:14
I don't have any intent to implement this but it's fun to play with ideas, and I was wondering about using assertions as a mechanism to add dependent typing via theorem proving to a language.18:15
(inspired by Nice's use of assertions in declaring things to be non null)18:16
oh, so you mean at compile time?
<DRMacIver>Yes and no.
The assertions would be present at runtime.18:17
Except when the compiler can prove that they can't occur
And when the compiler can prove that you're doing something which *will* cause them to occur, it would refuse to compile.
Additional possible variants could include a mechanism like "assert(foo) : MyException"18:18
Where MyException is thrown instead of the assertion error.
And you only need to catch it in circumstances where the compiler can't prove that the assertion will hold
<bonniot>i see18:19
you have an example with dependent types?
<DRMacIver>Well the example I had in mind is that this lets you e.g. declare contracts on methods that behave in a very similar way to dependent types.
e.g. if I begin a method foo(n) with 'assert ( (0 <= n) && (n <= 10) ) this is functionally equivalent to saying 'n belongs to the type of integers between 0 and 10'18:20
It's not full blown dependent typing.18:21
But it allows a significant chunk of it.
<bonniot>but if you accept the cases where the compiler cannot prove the assertion will hold, then the theorem proving is basically only an optimization for removing runtime tests, right?
<DRMacIver>To some extent. 18:22
But it's also a mechanism for preventing invalid code.18:24
Because you don't allow circumstances in which the compiler *can* prove that the assertion will fail.
<bonniot>i'm afraid that would be rare in practice
<DRMacIver>Yes, that's true.18:25
As I said, it's only an idea I'm playing with. :) I do that a lot.
<bonniot>it's good a thing to do ;-)18:26
<DRMacIver>I think the really useful parts would probably be the "I don't need to catch this exception because the compiler can prove it won't be thrown." time saving aspect, and an abundance of compiler warnings. 18:27
Alternatively there's no really compelling reason why the compiler shouldn't flat out forbid code which might allow the assertion to fail.18:29
At least given a sufficiently good theorem prover.
(I know very little about automated theorem proving though)
<bonniot>yes, that's the one in line with strict static typing
it's hard ;-)18:30
<DRMacIver>Yeah, I can imagine. :)
It's definitely on the list of things I want to learn about if and when I manage to con the universities into giving me a PhD offer. ;)18:31
have to hop out for a short time...
<DRMacIver>ok. Bye18:32
I swear I saw a jEdit plugin for Nice, but now I can't find it.
<bonniot>jedit nice in google? ;-)23:34
aha, but the page is stale...
<DRMacIver>The link is broken
Ok, found the links on the wiki. Unfortunately they point to the same place.23:38
<bonniot>seems xoltar has a new version of his site, so links are broken, but...
that's the plugin
<DRMacIver>Great. Thanks. :)23:40
(It looks like it will be some time before I have Eclipse working on this machine, so I figured jEdit would be a good compromise until then)23:41
<bonniot>having problems with eclipse?
The current version in the synaptic repositories is broken.
I could just install it manually
But frankly the way this computer currently is I doubt it could run Eclipse at more than a crawl anyway. :)
<bonniot>what are you running? debian unstable?
<DRMacIver>So I'll wait until I've bought a bunch of hardware upgrades, which should be early in the new year.
Edgy specifically23:43
(It's not just me being daft and not getting it to work. There's a genuine bug raised about this)
<bonniot>i have eclipse from edgy
<DRMacIver>What architecture?23:44
* DRMacIver is on AMD64
Which causes no end of grief. :)
<bonniot>aha, it's arch related?
<DRMacIver>I think so.
I'll double check
These problems usually are. :-/
Yep. AMD64 specific.23:45
how come you have a crawly 64 bit machine? :-/
not enough RAM?
<DRMacIver>Yeah, it's a RAM issue.23:46
This is a near minimal rebuild of when I set the old version on fire.
are you overclocking or what?
i also know 64bits means more memory use, unfortunately. since pointers are twice the size23:47
<DRMacIver>Nope. Poorly positioned boards and a lot of dust in the house. Dust built up around a capacitor where I didn't notice it.
<DRMacIver>Capacitor went boom, motherboard went up in smoke.
It's just lucky I was awake at the time, as it happened at 3AM. :)23:48
<bonniot>it could have started a real fire?
<DRMacIver>Probably not.
But not something I'd want to risk.23:49
<DRMacIver>It was certainly puffing out quite a lot of smoke before I yanked the power cord, but I think that was mostly dust.
In the end a surprising amount was salvageable. I actually got away with just replacing the motherboard (same CPU and RAM as before) and it more or less worked for about 6 months before I had to give in and replace the CPU and RAM as well.23:50
(There were niggling intermittent errors which I never pinned down that caused my computer to randomly crash every now and then)23:51
Anyway, enough of my boring flaming computer stories. :)
<bonniot>quite instructive ;-)23:52
beware of the dust
<DRMacIver>I think it was as much that there was a board very low near the base of the case which the dust got trapped in.
But yes, dust is evil.
On a totally different note, have you considered moving Nice over to SVN? 23:57
It's much more pleasant. :)23:58
</version control wars>
<bonniot>yes, i would be glad to switch23:59
just i don't know how easy it is to do on sf00:00
if it keeps the history, etc
<DRMacIver>Hm. Yeah, I don't know what migrating the history over is like.
<bonniot>i know svn provides tools for that
but i don't know how sf supports that00:01
<DRMacIver>The answer appears to be that it's not too bad but requires some fiddling00:05
Basically you need to manage the export from cvs to svn on your own machine.
<bonniot>i see
<DRMacIver>Then you can create an svndump of this and export that to a new sourceforge svn repository
<bonniot>you want to try it? ;-)
<DRMacIver>Sure. But if it takes me a long time it will end up having to wait for a week or so, as I'm not going to have much time to do it after today.00:06
And it's getting lateish. :)
<bonniot>no problem00:07
where are you from btw?
<DRMacIver>I'm more or less from the UK. :) I live in London.
Are you ok to handle the importing side of this? I of course don't have admin access to your sourceforge site. :)00:16
(If so I should have an SVN dump to hand over to you in a few minutes, assuming this doesn't die unexpectedly)00:17
<bonniot>yes. but it would be good to test the conversion before
* DRMacIver will test it before handing it over.00:18
<DRMacIver>(I'll just need to remember how commandline SVN works. :) I'm too used to using TortoiseSVN at work.)00:19
Ok. 'A few minutes' might have been optimistic. The conversion process is taking a while.00:21
(Just because there have been a lot of revisions to convert I guess)
development is rather XP-like, with lots of small commites00:22
<DRMacIver>XP is one of those things where I like some of the ideas but just can't buy into the hype. :)
<bonniot>in this case, i just mean working in small batches00:23
<DRMacIver>Yeah, I realised.
<bonniot>i'm not religious about it either
<DRMacIver>I naturally tend to a mix of the two styles I think - huge monolithic commits interspersed with a large number of much smaller ones.00:24
<bonniot>well, huge commits can happen if you make a big architectural change. but that should be rare...00:25
I guess I'm basing that on work, where I end up making a lot of architectural changes (because we're still building the architecture).00:26
Ah, conversion is complete.00:33
Will test it now.
<bonniot>did you see this?00:34
(you may want to remove the CVSROOT module, it likely doesn't contain anything useful for the future). Data cannot be readily removed from a Subversion repository.
Hm. Seems to be a problem.00:37
ok. It can't seem to read the dump that cvs2svn has created. 00:40
<DRMacIver>"Can't open file svndump/format" apparently.00:41
Maybe I'm doing something stupid. One minute.00:42
Doesn't look like it. I'll try something else.00:43
(Oh. cvs2svn is written in python. No wonder it doesn't work. ;) )00:51
* DRMacIver has a deep and only semi-rational dislike of python
How bizarre. I'm getting the same error when trying to load from a legitimately exported svn repository.00:56
* DRMacIver tries a different one to confirm
* DRMacIver glares balefully at the computer.01:01
<bonniot>maybe you need to sleep on it? ;-)01:02
I'm making one last attempt and then giving up. :)
As this is annoying me now.01:03
(I'm trying take 3 on a different computer to make sure this isn't some oddity of my local setup)
Same problem. I give up.01:14
I'll figure it out some other time. :)
<bonniot>yes, hopefully!
no problem, surely it will work later
<DRMacIver>Yeah. I'm sure it's just me getting some incantation wrong.01:15
Maybe I sacrificed the wrong sort of goat.
<DRMacIver>Anyway, I'm off to bed. night. :)
* bonniot leaves02:14