Search Results: "nate"

16 April 2007

Jonathan McDowell: In search of a HDTV PVR

As mentioned in the past I got a new TV this year. It's an LG 32LCD2DB with a native panel resolution of 1366x768. As well as the usual SCART/component inputs it has VGA and HDMI. Currently my homebrew PVR outputs to the TV via a full featured DVB card with onboard MPEG2 decoder, but this limits me to 720x576 output and a basic OSD. My current box is a PIII-800 with a basic onboard SiS graphics chipset, so it's not got the grunt to drive the TV directly itself. I'm thus on the lookout for an upgrade. Let's start with my constraints. I have a Silverstone LC-02 case. I'd previously planned to upgrade to something bigger, but the discovery that LinITX can provide a variety of riser cards to suit PCI-E/PCI as needed means I don't have to. The LC-02 will take a MicroATX board and provide me with 2 slots, one of which is taken up by the PCI DVB card. This box lives in my living room, so it needs to be quiet - the current incarnation is a bit too loud but I believe that's mainly due to using a standard heatsink+fan assembly, so I'm hoping that something specifically designed to be quiet will be better. An lirc dongle and wireless keyboard/mouse are already sorted. I'd like to expand the use of the PVR to be a more general PC as well; up until now it's just been a PVR, but being able to check email/IRC would be nice, as would the ability to play games. Up until now I've run VDR, which takes full advantage of the MPEG2 decoder, but I'd like to give MythTV a decent try. All of this points to wanting more than just a HD hardware MPEG2/MPEG4 decoder. First lets start with the graphics chipset options. The contenders seem to be ATI, Intel, nVidia and Via. From my reading ATI lack any form of XvMC support in both their Free and binary blob drivers, so we can discount them. nVidia have support, but only in their binary drivers. The Nouveau project have support on their TODO list, but I can't see any sign of it yet. I'd really rather avoid non-free drivers, so that leaves us with just Intel and Via. I really like the look of the Intel G965/X3000. They've opened up their driver development and it seems to be quite active from reading the Xorg mailing lists. However they don't have any XvMC support; Keith Packard on the xorg list in February says "For media purposes, the current drivers aren't taking full advantage of the hardware yet", though later on does say "XvMC is on several of our lists; I don't know when someone will pick it up and implement it". Unfortunately I get the feeling it's not a high priority; I've seen/heard several comments about the fact that any processor that'll get hooked up to this chipset will be more than fast enough to cope without the assistance. That may be true, but I don't want my CPU to be spending all its time trying to decode MPEG2 or MPEG4 at 1920x1080i while the GPU sits mostly unused. I'd much rather the GPU was used to the full giving me spare CPU cycles, or perhaps the ability to clock it a bit slower for common use cases, reducing power and heat. I'm keeping Intel on my list because I hope they do get round to proper support sooner rather than later. They've also talked about the fact the GPU is programmable which would make it perfectly possible to add MPEG4 acceleration to the chipset; that would be pretty sweet. It's a bit odd to end up with Via on the list. I mainly think of them as associated with MiniITX boards, but they do also produce various motherboards for Intel/AMD CPUs with integrated graphics. They managed to shoot themselves in the foot for a period of time by limiting the maximum accelerated resolution to 1024x1024, but recently they've released the CX700M /P4M900 chipsets which appear to do 2048x2048. The OpenChrome project have these up and running to a basic level from what I can tell, but work on XvMC support appears to be progressing with various patches and reports flying about on the list. So currently it looks like Via has the best option (albeit through the Free software community, rather than a concerted effort on their part), while Intel has something that could be very appealing if the driver was more complete. The other factor is the CPU. 3 contenders this time; AMD Intel and Via. My current PIII-800 is rated at 20.8W TDP. Modern processors are in general a lot hotter, but I need to keep in mind that I'm looking for a quiet machine, and that the case doesn't have a huge amount of room for big cooling systems. AMD's dual core chips all start at 89W or more, though some of their single core lower end CPUs are more like 67W. Of course the Intel graphics won't work with it and I'm not 100% sure Via has a suitable Athlon chipset at present either (the 2 I found were for Intel/Via). Intel's P4 offerings aren't much better for power consumption, with many of the highest end chips being over 100W. Core 2 Duo looks promising; 65W, so more than the current CPU, but a lot more grunt. Via come out tops here; 20W for their 2GHz top end processor. However this is only single core and compares poorly to the equivalent clock speed of Core 2 Duo. A MiniITX board with a 2GHz C7 and a CX700M would probably make a fine PVR, but I'm not convinced about there being enough grunt for anything else. The Via chipsets appear to have more active in-progress support for media acceleration, which suggests a P4M900 + Core 2 Duo. That's contrasted with what looks to be the more powerful X3000, that actually has a manufacturer who seems to want to get full Free support out there. I'm probably a couple of months off actually making a decision; partly because I want to watch how it all plays out in the hope that the Intel chipset will get some more support, or that the Via chipset will be proven to be reliable in operation. And assuming I do make a video chipset/CPU decision I then get the joys of trying to find a motherboard with DVI + SP/DIF. I know the G965 can do DVI out with an ADD2 card in the PCI-E slot, but I don't know if the P4M900 supports the same thing. I can't see an Intel MicroATX 965 board with SP/DIF out - there's an HD audio header, but this doesn't seem to be a direct mapping. Can I get a converter?

14 April 2007

Ben Hutchings: ACCU Conference

I've been meaning to attend the ACCU Conference for some years and finally decided to pay my own way for a couple of days this year. It was an opportunity to hear world experts on C++ and other programming topics and to a smaller extent to meet and socialise with other professional programmers. I attended the following sessions: Keynote: Improving Collaboration in Open Source Projects, Mark Shuttleworth This was a somewhat surprising choice of speaker and subject since I think most attendees work on proprietary software, but I think any sensible developer in the proprietary world will try to build on free libraries under non-copyleft licences, where appropriate. Mark talked about governance and leadership in "open source" projects (actually praising Debian for having a clear constitution) and about the need for good communication between projects, for example about release schedules. He seems to have accepted that Launchpad cannot be a single hub, and called for standard formats for, for example, exchanging information about related bugs between bug trackers. But it doesn't sound like he's ready to take the lead on that. Choose your Poison: Exceptions or Error Codes, Andrei Alexandrescu Andrei looked at the strengths and weaknesses of various error reporting mechanisms in C++ and introduced a technique for making error handling more flexible. Normally a function is designed either to indicate errors through its return value or to throw an exception on error. If a function returns an error indicator, it's easy for callers to ignore it. If it throws an exception on error, then a caller that provokes errors more often than the called function's author anticipated pays a high cost in processing time for those errors. Andrei's solution involves a class template Likely<typename T> whose instances hold either a return value of type T or an exception. A function that can fail has a specialisation of this template as its return type. The caller can check for failure if it knows how to handle it, or it can ignore it - in which case the conversion to T or the destructor will throw the exception. This is clever but doesn't seem to be entirely satisfactory. The destructor which throws does first check that no exception is already being processed, avoiding collision of the two exceptions and consequent abrupt termination of the program, but this can result in errors being unexpectedly ignored. Introduction to Component-Level Testing, John Lakos A marathon 3-hour talk on designing and testing software, particularly C++ programs (the subject of his well-known book) as a set of well-defined components. Lakos first defined these components as being "physical" i.e. sets of source files - normally a header file defining an interface, an implementation file, and a test driver file. They may also include metadata for the build system. He talked about the value of reusable components (as if this wasn't obvious!) and the risk of introducing circular dependencies - which essentially turn many components into one and reduce reusability - if we fail to keep track of dependencies. Software built out of components can be viewed as a hierarchy or stack defined by dependencies. In a large system, components with similar dependencies and dependents can be grouped together into packages or package groups to simplify a view of these dependencies. He explained that the test driver's dependencies count just as much as the implementation's, because we cannot reasonably test a component until we have tested its dependencies. Test drivers should also be written to avoid depending on environmental settings and configuration, so far as possible. Finally, and perhaps most importantly, he spent a long time talking about how to construct test cases and test data. I might try to summarise this in a later entry if anyone's interested. The Appliance of Science: Things in Computer Science that every practitioner should know, Andrei Alexandrescu Andrei began by complaining that OpenOffice Impress was even worse than PowerPoint, but being able to use Linux (specifically Ubuntu) more than made up for the pain. He briefly presented four key ideas that he believes programmers should understand and be ready to make use of: Writing for ACCU (BoF) I think I've been convinced to write an article about standardisation of multithreading in C++. C++ Threads, Lawrence Crowl Crowl gave an overview (similar to this) of the extensive work that's been done on standardisation of multithreading in the C++ language and library. This is one of the most important features in C++0x due to the increased parallelism mentioned above. The current semantics of multithreaded programs are not standardised, resulting in subtle but potentially serious differences between current C++ implementations that support multiple threads, and in the need for assembly-language code in programs that use lockless synchronisation. Much of this is also relevant to C and is being considered by the C standard committee. C++0x Initialisation: Lists and a Uniform Syntax, Bjarne Stroustrup Stroustrup recapped the 4 forms of syntax for initialising objects in C++, some inherited from C and some necessarily invented for C++, none of which are entirely generic. He noted the lack of a simple syntax to initialise the elements of containers, which violates the general principle that class types should have the same status as built-in types in C++. He then introduced a new initialiser syntax that he and others have defined for C++0x, which is a brace-enclosed comma-separated list of values, similar to that used for arrays and C-style structures (aggregates). Container types can define a constructor with a parameter of type const std::initializer_list<T> & and when constructed with this new form of initialiser they will receive this wrapper for a constant array of element values. For types that do not, the values in the list are treated as arguments to some other constructor, if one matches. Otherwise, for compatibility, this may be treated as aggregate initialisation. C++ Standard Library report, Alisdair Meredith There was far too much information here for me to even begin to summarise. Suffice to say there are lots of good things coming bu the library committee will have its work cut out to get them all properly specified in time for the Committe Draft coming late this year.
I also met old friends and new, put faces to names from newsgroups and books, and got too little sleep.

13 April 2007

Arnaud Vandyck: libhibernate-java Take 4, fop and other updates

    • New packages
  • qdox_1.6.1-1 (#323043 and #418673)
  • xmlgraphics-commons (#418896)
    • New upstreams
  • commons-io: #418973, #397567
    • Bug fixes
  • libgef-java: #418865
  • read more

    Erich Schubert: Init followup

    Gunnar Wolf commented on my recent series of init script posts. Thanks for the feedback.The thing is that I've been doing a lot of Debian stuff these days (such as our GSoC coordination, and lots of stuff you saw in this blog). But I shouldn't... instead I should be trying to finally get my diploma thesis done.I had my exams last july. If I had been focused, I could have been finished with my degree last christmas. Now it will likely by this fall. :-( All that is remaining is my final thesis. It should be written in 6 months, but I still havn't submitted my topic yet. So if you are wondering what took me 8 months already: I investigated two topics, but they didn't work out. Then I started researching for my 'current' topic, and I have a vision for it, but I still havn't managed to convince my professor (which of course is largely due to me not being able to convey this idea, and that the topic is in information management and representation, where it's probaly often hard to find a solid theoretical part. I have examples I'd like to do, and I hope they are actually convincing, but I have no idea how to 'prove' something here; it's too much about social aspects and human perception I guess, and I'm not really qualified or capable to do solid research in that field.)(And as you can probably imagine, I'm pretty fed up with studying now. A year ago, I'd have considered to go for a PhD afterwards, but now I just want to get out, and work on my projects.)Anyway, I got distracted. Back to the init topic.I already posted this link: Init Hackfest, as well as a pointer to the initscripts-ng mailing list. I'd really like to get this topic on it's way for lenny. So please, join this effort. While I'd like to push it, I shouldn't; on contrary, I should suspend my Debian efforts.As for your (Gunnar) suggestion on how to handle multiple inits: what's wrong with just including multiple init scripts in one package? They are not particularly large and compress well. A single init script package might already be bigger than all the init scripts.The problem is more on how to write these init scripts; by the time we're done with this project, we might actually have hit 1000 init scripts. Yes; I didn't just make up this number: packages.debian.org has 890 hits for /etc/init.d; the init-like scripts in /etc/dbus-1/event.d not included. So if just want to add support to 5 alternate init systems, this means we would need to write 5000 new init scripts. Ouch. So we maybe should convert them to 1000 meta-init-scripts instead, and generate the 6000 real init scripts from them.Please join the discussion, and lets get this project going, despite having to face such scaringly high numbers...

    Evan Prodromou: 22 Germinal CCXV

    A lot of people have asked me about the Tim Wu piece in Slate about Wikitravel. I've commented already about the article in Wikitravel's Logbook: 8 April 2007. The upshot: Wu got a lot of things really wrong about Wikitravel (like saying we didn't have any hotel listings for Bangkok). But if our readers get things wrong, that means Wikitravellers need to do some more work to help them get things right. User errors are developer errors writ large; we can do better. But I think Tim Wu missed the main reason Wikitravel guides will always be better than proprietary guides: they are Free Cultural Works. Where I come from, that means a lot. I wrote to Tim about his article, and he responded really kindly. The thing I liked most is that when he got home, he updated Wikitravel with the information he picked up on his trip to Thailand. That is pretty cool. I'm not taking others' responses to the article too seriously. Wikitravel got a Webby Award nomination for Best Travel Site the same week. As Tom Wolfe said, "The lead dog is the one they always try to bite in the ass." And Oscar Wilde: "The only thing worse than being talked about is not being talked about." (Thanks to Hugh!) tags:

    Off to San Juan We're getting prepared this morning to head out to Puerto Rico for the first annual World-wide Wikitravel Get-together. Our flight leaves at 2:20PM, so we've got kind of a leisurely morning to get ready. As usual, we're pretty tense: what are we forgetting? And I usually get hung up on unnecessary stuff to deal with. I should probably print out the Spanish phrasebook from Wikitravel, because my Spanish is pretty rusty. And I should download all the WT pages about Puerto Rico destinations to my laptop, just to know where we should fill in. And we can't find the charger for our camera's battery. And I want to bring a certain pair of cargo pants, but there's a button missing. Do I have time to sew on another? Of course, all these anxieties melt once we get out of the house and into a taxi to the airport. Once you can't do things, you stop worrying about what you should do. I think. The more I learn about Puerto Rico, the more fascinated I am. San Juan (Puerto Rico)'s Old Town is a UNESCO World Heritage site. The giant telescope at Arecibo is world-renowned as the SETI site. The islands of Vieques and Culebra are isolated and fun, and Fajardo and Rincon has world-class surfing. My friend Biella Coleman gave me a great list of travel tips for San Juan and Culebra, which have been a big help in our planning. OK, enough blogging: gotta get to work sewing on that button. (I've been stalling long enough for Maj to have found the camera charger under a baseball hat. Yay!) tags:

    12 April 2007

    Erich Schubert: System init - part #3

    Today's post (previous parts) tries to show what benefits other init systems can offer.I'm picking 'minit' as an example; not because it's the ultimate solution or anything, but because I happen to know it quite well. I used to be the package maintainer for some time, and I've also used it on an embedded system (where it was a perfect match). However, it's not very distribution-friendly; it's great when you can invest some time into configuring it (such as when building an embedded system) but not when it should ideally work automatically out of the box. The Debian package is still there, but it's orphaned. Still it's well written, clean code; there shouldn't be any bigger bugs in there.The first thing to notice is that minit is tiny. It's statically linked, but only about 6.5 kb. Regular init is 86 kb plus some libraries (despite actually not doing much during init!). This makes it very well-suited for embedding.But now for the benefits of minit over regular init:1. Service monitoring. This is the biggest point: minit will keep an eye on the services and restart them when needed. (Another thing very useful in embedded situations, btw.)Minit doesn't use the start/stop paradigm of sysv/shell-style-init. Instead it has a "run" script for every service. If a service is flagged as 'respawn', it will automatically be restarted when the run script quits; therefore the applications should not background themselves. This offers some benefits, for example the init process will be notified by the kernel of a termination, and can immediately respawn the service; in contrast to other monitoring systems suchas monit it doesn't rely on 'busy polling'.2. Dependency handling. Minit handles startup dependencies. If a service lists another service as a dependency, it will bring that service up first.3. Parallel startup. Unless an ordering is given via dependencies, minit will start the services in parallel.4. Control apps. In minit, you don't start a service by running some random shell script. Instead you call "msvc -u servicename", which will signal minit to bring up the service (and it's dependencies). This would (there currently is no policy for minit) be especially useful in SELinux, but it also allows to e.g. give a user the permission of running "sudo msvc -u" without introducing a huge security hole, since this cannot be used to execute arbitrary scripts. "msvc" can also be used to check if a service is up. (Another benefit for embedded systems, since that removes the need for pid files, which then need a ram (writeable) filesystem)I'll also give an example for a minit service:A service is represented by a directory in /etc/minit which can contain various files. I'm going to look at getty/1 example; which will bring up a console login on the first terminal. There are three files: If the service would need it, there could also be a file called "depends" listing service dependencies.This allows minit to start the getty with no overhead. There is no shell script being executed or anything (note: sysvinit also does this for gettys, but it's not being used much for other services).Of course minit isn't perfect. I've already said that it isn't particularly distribution friendly. This is because it uses a lot of magic files (e.g. an empty file named 'respawn' to flag a service as needing to be respawned), and it's configuration files aren't easy to handle automatically. The often frowned-upon 'symlink farms' of sysv-shell-style init are much better here.Another thing that is missing from minit is an automatic rollback of dependencies. If we told minit to bring up service 'a', which lists dependencies 'b' and 'c', minit will bring these three up. If we tell it to shutdown 'a', it will however not shutdown 'b' or 'c'. And unfortunately, even if we shutdown 'b', it won't shutdown 'a'. If you want a more complex dependency handling (or things such as runlevels), you need to do this externally. (An example is my 'enitdir' app, it adds runlevel support to minit, and allows switching of runlevels by replacing a symlink; Services are added and removed from runlevels by adding a symlink to the service into the runlevels directory. By using dnotify, this also takes virtually no CPU time.)Minit also lacks a differentiation between a 'started' and a 'running' service. It has support for 'sync' services, such as e.g. mounting a filesystem. It will wait for this operation to complete before it starts services depending on it. However, there are services that will continue to run, while not being instantly available when the exec() was called. Sometimes it would be nice if a service could go into a 'started' state, then do some cleanup work, and then when actually running the real service signal minit that it's now 'running'.As a last malus, minit won't print progress messages to the console. A minit boot is pretty much silent, directing it's output to some logging processes. There are good reasons for this (since services are started in parallel!), but it makes debugging harder, and users might be wondering what their system is actually doing (though some users prefer to see a colored 'busy' bar)...I guess this concludes this series of blog posts. Maybe someone can follow up with some details on upstart (which seems to be the most promising init replacement)? I hope to have given an impression on where there is room for improvement in our current init to one or the other. Now we just need some people to actually work on a better support for other inits in Debian...

    MJ Ray: BBC Radio 4, Again, Again

    Kris Marsh commented:
    "Thanks for the blog, I'd never have known about the BBC4 open source slot otherwise! Unfortunately I missed it, but I did notice that it's available on BBC's "listen again" feature "
    So, what did you think of it? Post comments to my site or to fsfe-uk.

    Erich Schubert: Apologies if I'm breaking a planet

    I've done a needed upgrade to my blog software. In this process, I've also been changing my blogs GUIDs. Unfortunately, this probably means that some planets or feed readers will recognize all of my postings as 'new'. Sorry about that. I'm not sure if I can somehow prevent it from happening.Every now and then I receive a mail from someone complaining that the links to my blog entries are broken. Well, they aren't. The link tag has an appropriate value. However some applications (usually involving planet) prepend the feeds base URI to the GUID field or use it in other RDF places. And then some readers seem to not know about the link tag and use that instead. So I'm now using the permalink as GUID, so it should be a bit easier for some people, since they now can just click on my entries.

    11 April 2007

    Stefano Zacchiroli: post etch frenzy

    Post-Etch Frenzy: Ocamlnet 2.2.7 in Unstable Ok ok, ..., I admit it, I'm yet another victim of the post-release frenzy: right now I'm uploading to unstable the long overdue packages of Ocamlnet, 2.2.x series. Since the former upload to experimental there were 3 micro releases (now we are at 2.2.7), which also added support for the apache connector for CGIs (which unfortunately doesn't yet build cleanly with Debian's apache2 :-/ I'll have a look at it in the near future). In the meantime the post-etch madness continues: with the help of other fellow DDs from the Debian OCaml Task Force (thanks for your help Ralf!) I'm working on the packaging of the beta of OCaml 3.10.0. Expect an upload to experimental in the next few days. All this is tiresome though, enough for today, time for some good old sci-fi book ...

    Kai Hendry: Webconverger 2.4

    Korean Webconverger split 2.4 I’ve just released Webconverger (Web kiosk) USB&ISO versions built with stable Debian etch. Webconverger has received some good feedback and press. I would like to thank Daniel Bauman for his rather excellent Debian Live work on which Webconverger is based. I was hoping that Webconverger could support every locale, now it looks like I need to produce a separate ISO/IMG (or at least apt-get hooks) for every locale. One reason is that Iceweasel/Firefox extensions don’t scale very well. Try install every locale and dictionary extension. I dare you. :) Sidenote: I wonder why no one has packaged the dictionaries for Iceweasel. In other news, I’ve been playing around with scim (keyboard switcher) and Korean locales. It seems to work though the title bar didn’t render hangul characters right in dwm. After some investigation I discovered there isn’t such a thing as a single “generic” Unicode font. This came as a shock to me. :) Typical ttf only have 65536 glyphs, so no one font will do. Jeff Zhang also informed me about free Unicode fonts. Though I think especially in CJK environments proprietary fonts are unfortunately more common. Or I don’t know why microsoft-gulim isn’t in msttcorefonts. Anyway the Korean version of Webconverger turned out OK, though I doubt any Koreans will be using it. It’s all sadly ActiveX out there. My package wordpress 2.0.10 didn’t quite make it to etch in time as I was waiting for CVEs! 2.0.10 will be coming soon though… It always amazes me how much work can get done in breaks like Easter. It’s great that etch is out. And whoa, the weather is great.

    MJ Ray: Satellite TV and Media Links for 2007-04-11

    Ofcom publishes research on media literacy
    Analysis of a research report: "Certainly a useful document to have on hand, if only to deconstruct."
    Karen Bremner - The Apprentice Series 2
    A new art form: go on a reality TV show, start blogging to raise profile, get hired by Old Media, then leave the site to bit-rot. How many of these "reality TV star headstones" sites are there now?
    predicts problems and confusion for consumers
    If anyone doubts how much big media gets bad PR from trying to use their big influence to direct the market (such as making their films only available in their format), check the first comment: "I'm waiting for the corporate idiots to decide"
    xmltv, was: [Debian-uk] Getting wired in Manchester
    Another thing on my "must try that when I get my DVR built" list.
    theLargePrint.com The New Media Landscape and the BBC's Lost Horizon
    Nice criticism of BBC's link-up with anti-competitors. I recently wrote about the BBC-Google link, which raises some similar problems.
    BBC NEWS Business Fewer charges for website content
    Figures from 2006 (I'll do media linkposts more often in future).
    Time to read the papers?
    I only get time to read one paper per week, unless I'm travelling.
    Number 10: Tony Blair Interview with Stephen Fry
    Fantasy TV shows number 10: A bit of Fry and Blairie.
    BBC NEWS Technology Broadband switching set to ease
    They say new rules came in on 14 February, but sites like moneySavingExpert.com are still full of tales of woe.
    We the undersigned petition the Prime Minister to ban tv competitions/quizzes which charge extortionate caller rates (eg The Mint).
    Sign this to clear UK digital TV of all these scam quizzes. I see that after just a taste of humble pie, itv play is back on air overnight on itv1.

    10 April 2007

    Evan Prodromou: 20 Germinal CCXV

    I'm really excited this morning. Wikitravel has been nominated for a Webby Award in the Travel category. It's amazing to get this kind of recognition for the work that our community has done over the last four years. I think that Wikitravel has a good shot at winning the award. I also hope that the Open Source and Open Content community, as well as wiki enthusiasts, will turn out to vote for us in the People's Voice Awards (open to voting by the entire Web community). tags:

    AboutUs.org has OpenID Looks like Portland (Oregon)-area startup AboutUs has implemented the OpenID extension for MediaWiki. Meaning that anyone can log into AboutUs with an OpenID! This moves AboutUs into a nice single-signon network with Wikitravel, Wikevent, and wikiHow, as well as a number of other OpenID-enabled sites. Great for them. tags:

    Kevin Rosenberg: E-mail loss

    I sufferred a disk failure today involving the /home partion of my main communication/development system. Fortunately, I keep my home directory in subversion, so I didn't loose any files that I keep updated in my respository. This, however, does not include my email files. Normally, this would not be a problem at all since all my systems are backed up nightly on a network backup server. Unfortunately, the partition that backs up my failed drive filled to 100% in mid-Februrary, so my email was restored to only mid-February. The main reason for this post is to give notification that if you sent any email to me over the last 2 months, it's been lost, so please do resend. Especially, resending of patches would be appreciated.

    9 April 2007

    Daniel Burrows: Latest Shiny Geek Toy: coq

    So, one of the reasons I've been a bit uncommunicative the last few weeks is that I've been getting my head around Coq, maybe one of the most fascinating pieces of software I've played with in a long time.

    What is Coq? I don't know if I understand it well enough yet to give a complete description (the Coq tome only arrived in the mail on Friday and I have yet to make it past the introduction, what with taxes and so on). Here's my best shot:

    Coq is a programming language where you write proofs as functions taking proofs of their preconditions and producing proofs of their results. That is, a proof that "If X is an integer, then X-1 X" becomes a function that accepts a proof of "X is an integer" and produces a proof of "X-1 X".

    You can manipulate logical expressions more or less the way you expect. For instance, if you have in your hands a set S of natural numbers and a proof that "forall nonempty sets T of naturals, T has a least element", then you can bang these together to produce the least element of S (or rather, a proof that it exists).

    I don't think this describes the theoretical underpinnings of Coq, but it does describe my experience of actually using it to prove stuff.

    To get the hang of Coq, I'm working my way through basic automata theory -- regexps are done, but I couldn't work out how to express some finiteness constraints on FSMs without generating a lot of extra typing; hopefully the Coq book will have some hints. Once that's done, I'm actually tempted to try something more ambitious. [snip long digression] We'll see ... watch this space :).

    It was a real rush, though, to code up these theorems and watch the computer verify them. What really fascinated me was how close to being a practical tool this is. Coq isn't at all a toy -- without quite getting all the theory yet, my intuition is that it can probably cover anything you can express in the predicate calculus (with sufficient amounts of typing, anyway), and while there are a few shortcomings, it's almost (IMO) at the point where anyone who knows some formal logic and has a little patience can prove interesting stuff. Even more suggestive of possibilities, there's a project (which I sadly haven't had time to look at) that integrates Coq with OCaml, so you can have proofs about your OCaml code verified at compile-time!

    I could go on and on ... anyway, this is a really cool tool and I'd encourage any mathematically-minded person to give it a spin. The only sad thing is that I doubt I'll ever have the opportunity to explore this stuff in my day job unless/until I go back to school :-(.

    Shortcomings of Coq specifically and the whole concept of correctness proofs on programs generally have been moved to a future blog post that may never appear depending on how ambitious I'm feeling this week. Rest assured that I'm aware of (some of) them, I just hit my self-imposed length limit.

    [0] the reason being that I could only prove correct the formal underpinnings of the resolver; in practice, a lot of the bugs are in the interface to apt, or in apt itself, and I can hardly prove that code correct.

    Sam Hocevar: Election results

    Okay, I guess I m expected to say something. You ll probably notice I m not exactly bouncing around in a great explosion of joy. I ll keep that for the upcoming obligatory yay for Etch post. As much as I m saddened by a few reactions of perplexity or sometimes even bitterness, I hope the ha, in your face! attitude targeted at other candidates will eventually fade out, too. I really didn t think I would win (at least before all those people started e-mailing to tell me they voted for me). My initial goal was only to make people think I could win, so that other well-placed candidates would pick up the good stuff in my platform or adapt to it. I didn t really care about me being DPL. Well, apparently this didn t go exactly as expected and here I am. That said, I m of course happy that my candidate of choice won :-) And it s good that we had more voters than last year. I d also like to thank all other candidates for running. Despite disagreements and given how much I advocated teams in my platform, there s obviously things we ll be able to do together, I just don t know the details yet. I have already been offered help on many topics, including from people with whom I ve disagreed or even quarreled and that s really heartwarming. It will be a great year. For the datamining lovers here, you may want to use this alternate tally sheet that makes grepping more meaningful. Votes are rewritten as a comma-separated preference list: 3567,4,1289 means ranked options 3, 5, 6 and 7 equally, then option 4, then options 1, 2, 8 and 9 equally and could be a --19111-- or a 331211133 vote (which mean exactly the same to the voting software but not necessarily to the voter). To know for instance how many people ranked NOTA above all other candidates, use grep '^9,' (that s 19 people, by the way). To know how many people put at least 5 candidates below NOTA, use grep '9.*,\([1-8].*\)\ 5\ ' (and that s 119 people!).

    Erich Schubert: Renaming applications

    You probably have read it alread Gaim will be renamed to Pidgin. Most likely because of AOL being unhappy with them using AIM in their name (although they support a dozen other messengers as well; getting rid of AIM in the name was also 'wanted' by the Gaim developers I guess). However, such software renames eventually cause some problems. For example, will the API also be renamed? Will libgaim become libpidgin? Will the DBus interfaces change their name? A dozen of applications might be affected by that, including the popular AdiumX messenger for OSX. (One of the prettiest I've seen so far, btw.) Other examples of such renames (and the problems caused by that) is the Mozilla chaos. Mozilla doens't allow to distribute modified versions of Firefox or Thunderbird under these names, so Debian has to replace the names (though most of our patches at some point are adopted by upstream, or they'd be okay with them, Debian also has the requirement that our users must be able to do their own modifications!). This is why etch just shipped with "Iceweasel" and "Icedove" instead. However some web sites don't test for the browsers "Gecko" version, and for example Google Groups, when trying to set the profile image, tells me I need to run Firefox or Internet Explorer. Though I'm pretty sure the function would just work fine with both Epiphany (my primary browser) and Iceweasel. The transition from "cdrecord" to "wodim" was a bit smoother. On the one hand, many application were already expecting functionality not present in the "official" cdrecord (and yes, Joerg, I know that your opinion might differ on that point - I don't care, nor does anybody else I know). On the other hand, it mostly affects programs included in the distribution, so they can be easily handled. There aren't random websites testing for it either, and custom scripts written by users can probably handled via a wrapper (this is much more difficult for libraries I guess, or the DBus API of Gaim. Fortunately for Gaim, these interfaces aren't used much, so it can be solved with a simple search and replace and recompilation in affected applications). I think when more distributions switch from Firefox to Iceweasel because of realizing that it might be important to some of their users and recommend Epiphany because of it's smoother user interface, we might also see less websites doing incorrect browser capability detection.

    8 April 2007

    Alexander Schmehl: It's done!

    Etch is released... Time for some thanks... Thanks developers, who make it possible; thanks d-i people, who make it installable; thanks to translators, who make it available; thanks r-m, who keep it coordinated! Special thanks to Joey, for going on vacation right in time so I have the honour to announce Debian releasing... twice in 24 hours! Very special thanks to Meike, who didn't cared that I spend the last days translating the release notes, testing different images (and killing a very important machine while doing so), compose announcements, coordinate translations, finally sending out, answering some replies and forgeting to buy her some sugar eggs. I would like to point out, that the last mentioned thing is not a matter of course, considering that we had guests during the last days, and she had to play host all for herself! Shame on me ;)

    Sam Hocevar: Election results

    Okay, I guess I m expected to say something. You ll probably notice I m not exactly bouncing around in a great explosion of joy. I ll keep that for the upcoming obligatory yay for Etch post. As much as I m saddened by a few reactions of perplexity or sometimes even bitterness, I hope the ha, in your face! attitude targeted at other candidates will eventually fade out, too. I really didn t think I would win (at least before all those people started e-mailing to tell me they voted for me). My initial goal was only to make people think I could win, so that other well-placed candidates would pick up the good stuff in my platform or adapt to it. I didn t really care about me being DPL. Well, apparently this didn t go exactly as expected and here I am. That said, I m of course happy that my candidate of choice won :-) And it s good that we had more voters than last year. I d also like to thank all other candidates for running. Despite disagreements and given how much I advocated teams in my platform, there s obviously things we ll be able to do together, I just don t know the details yet. I have already been offered help on many topics, including from people with whom I ve disagreed or even quarreled and that s really heartwarming. It will be a great year. For the datamining lovers here, you may want to use this alternate tally sheet that makes grepping more meaningful. Votes are rewritten as a comma-separated preference list: 3567,4,1289 means ranked options 3, 5, 6 and 7 equally, then option 4, then options 1, 2, 8 and 9 equally and could be a --19111-- or a 331211133 vote (which mean exactly the same to the voting software but not necessarily to the voter). To know for instance how many people ranked NOTA above all other candidates, use grep '^9,' (that s 19 people, by the way). To know how many people put at least 5 candidates below NOTA, use grep '9.*,\([1-8].*\)\ 5\ ' (and that s 119 people!).

    Gustavo Franco: Etch, Lenny and the future.

    Etch is out, thanks for all those who worked hard during the release. Time to party, but for those that are hungry to push their packages from experimental to sid, make sure to not start tons of not coordinated transitions and breakage, if in doubt about what to do ask the release team (debian-release@lists.debian.org). Don't make sid and testing such a nightmare from the first day, keeping uploading new upstream releases to experimental for a while, ask for testers (tons of them) and move to sid non-RC buggy stuff now! Help us get Lenny ready.

    Lars Wirzenius: Debian: It's full of chars!

    The etch release is imminent, so I thought I'd run sloccount on an unpacked Debian source tree. I wrote a little script that downloads and unpacks all Debian source packages. It does dpkg-source -x only, no debian/rules unpack or such, since that isn't standardized. The result is a source tree that is 46 gigabytes. Unfortunately, there is something in that tree that makes sloccount fail. It reports a mere 45 million lines of code, which is about 1022 lines per kilobyte. (Later, I'll narrow it down and report an actual bug. For now, the best I have is "something in Debian breaks sloccount".) Sloccount would give fairly good results, and it would exclude, say, JPEGs, of which there are 455. However, in this situation the best I can easily come up with is a sum of running a plain wc -l on each file, and that sum is 1005505921. That's just over one billion lines of code, in 2868448 files, or 350.54 lines per file, on average. Disclaimer: that sum includes many non-source files, such as the JPEGs, and a number of packages don't actually unpack properly with dpkg-source, you have to run some variant of debian/rules unpack. However, I'd be willing to bet the number is in the correct ball park. We can get better results once sloccount gets fixed.

    Next.

    Previous.