David's blog

To content | To menu | To search

Monday, March 29 2010

Status of OCaml packages on Ubuntu Lucid Lynx (10.04 LTS): transition to OCaml 3.11.2 finished

By d. on Monday, March 29 2010, 13:00 - Free Software / Libre

I don't know who are responsible for this but the OCaml packages of Ubuntu Lucid Lynx 10.04 LTS have all transitioned to OCaml 3.11.2 on main architectures (amd64 and i386). A big thank to the mysterious developer(s)! Even for secondary architectures, all packages have transitioned to 3.11.2 except 3 packages on armel: coq, ssreflect and why.

Of course, having a source OCaml package compiled with the correct version of the OCaml compiler does not make it automatically working so I encourage you to test your preferred Ubuntu OCaml packages in Lucid.

If we now compare the set of source packages available respectively on Debian Unstable and Ubuntu Lucid, the situation is not so perfect. On the 145 OCaml packages available in Unstable, 21 are not at the same stage in Lucid.

There are 5 packages simply not available in Ubuntu:

  • clang 2.6-3
  • llvm 2.6-8
  • llvm-snapshot 20100312-1
  • obrowser 1.1+dfsg-4
  • unison2.27.57 2.27.57-2

There are 11 packages that have been updated in Unstable but not upgraded in Lucid:

  • Package Unstable-version Lucid-Version
  • approx 4.2-1 4.1-1
  • camlpdf 0.5-1 0.4-4
  • coccinelle 0.2.2.deb-1 0.2.0.deb-1ubuntu2
  • graphviz 2.26.3-3 2.20.2-8ubuntu3
  • ocaml-csv 1.2.0-1 1.1.7-2
  • ocaml-ssl 0.4.4-1 0.4.3-3
  • ocaml-text 0.3-1 0.2-3
  • ocsigen 1.3.0-4 1.2.2-1
  • pgocaml 1.4-1 1.3-3
  • postgresql-ocaml 1.12.4-1 1.12.1-2
  • unison 2.32.52-1 2.27.57-2ubuntu2

And lastly there are 5 packages that had minor updates or packaging bug fix in Unstable but not in Lucid:

  • Package Unstable-version Lucid-Version
  • nurpawiki 1.2.3-4 1.2.3-3
  • frama-c 20090902+beryllium+dfsg-5 20090902+beryllium+dfsg-4
  • ocamlgraph 1.3+debian-2 1.3+debian-1
  • sks 1.1.1-2 1.1.1-1ubuntu2
  • ssreflect 1.2+dfsg-4 1.2+dfsg-3

I don't know what to do about those packages or if I can even do anything. According to Ubuntu Lucid release schedule, we are reaching Beta 2 Freeze (on April the 1st) where uploads for packages in main and restricted are held in the queue and are subject to manual approval of the release team.

Do you have any advice?

Beside that, we still have 124 OCaml source packages in good shape in Lucid!

5 comments

Thursday, March 18 2010

Looking for a C software for Formal Verification

By d. on Thursday, March 18 2010, 13:00 - Software Verification / Vérification de logiciel

As you probably know, I'm a huge fan of Formal Methods: use appropriate Mathematics and tools to ensure a program is correct in all possible situations. In other words, bug free software... well, sort of. :-)

The interesting side of this is that tools to apply Formal Methods have improved a lot and most of them are now Free Software. I'm maintaining a list of Free Software tools for Formal Methods (it is a wiki, you can update it!).

I would like to make an experiment with Frama-C and its plugins, especially Jessie. Frama-C is a framework for static analysis of C programs developed at CEA. Combined with the Why and Alt-Ergo tools, you can prove some properties on real C code (absence of integer underflow or overflow, absence of out-of-bound accesses, absence of NULL pointer de-referencing, program's specific properties, etc.). All those tools are Free Software and are developed in OCaml. And they now are available in Debian and Ubuntu!

I made a simple experiment last year but I would like to make a more elaborated one.

Therefore, I'm looking for a piece of C code with following criteria:

  • Free Software: I'm interested in improving software for the whole humankind; ;-)
  • Pure C code, no C++. If there is some assembly, I could work around for example by re-writting corresponding C function;
  • Code of moderate size, a few thousands line at most. It could be a sub-module or subset of a bigger code;
  • Code using mostly integers and pointers, few strings (aka char *)[1];
  • Verifying some properties on this code would be "interesting". Several possible reasons: for security or safety reasons, because the code is used in an embedded platform on which modifications are difficult once in production or simply because this code is used a lot.

If you know some software that fills those criteria, let me know through a comment or at dmentre@linux-france.org!

Notes

[1] Frama-C is a bit slow to handle strings and it can become cumbersome.

3 comments

Wednesday, March 10 2010

Standing on the shoulders of giants: MapOSMatic in a sea of Free Software

By d. on Wednesday, March 10 2010, 13:00 - Open Street Map

One thing that stroked me after the two hackfests we made to develop MapOSMatic: the little amount of code we really developed! In fact, we are re-using a lot of other Free Software.

Using the excellent sloccount, I tried to get some figures. MapOSMatic is about 3150 lines of code, 90% made of Python. MapOSMatic dependencies count for more than 600,000 lines of code, counting PostgreSQL, PostGIS, Apache 2 httpd, Django framework and some small libraries.[1] So we only developed about 0.5% of the code needed to run the MapOSMatic service. And I obviously do not count the OpenStreetMap data itself, which is about 70 GB!

That's why we can say, as most of software developers, that we are standing on the shoulders of giants: we are re-using knowledge, hard-work and polishing of a lot of other people. MapOSMatic is a glaring example of this fact and of the power of Free Software.

Notes

[1] Counting all MapOSMatic dependencies is nearly impossible: it is hard to draw a line between what is part of the system and what is a specific dependency of MapOSMatic (e.g. Python).

Thursday, January 14 2010

Quick news: OCaml on Ubuntu Lucid and MapOSMatic

By d. on Thursday, January 14 2010, 13:00 - Free Software / Libre

OCaml on Ubuntu Lucid

I have updated my scripts to compare Ubuntu OCaml packages to Debian ones. This time, I'm comparing Ubuntu Lucid against Debian testing, as for Lucid packages are imported from Debian testing (because Lucid is a Long Term Support release).

You'll find all the generated files here: http://bentobako.org/ubuntu-ocaml-status/raw/

MapOSMatic

As you have probably seen, we have done major improvements to MapOSMatic during Christmas, at both the web site level and the rendering level. I won't go into details, just read our initial announcement. Since then, we are continuing our improvements on maposmatic web front-end and ocitysmap back-end, with a new web site layout, translation of web site and maps in many languages (Arabic, Brazilian Portuguese, Catalan, Dutch, French, German, Italian and Russian). Many thanks to the numerous contributors!

We still have a lot of things to do or bugs to fix but the feedback is very positive and rewarding! Many thanks!

one comment

Thursday, December 3 2009

Installation of Linux Ubuntu Karmic Koala (9.10) on an ASUS UL30A-QX090V laptop

By d. on Thursday, December 3 2009, 13:00 - Free Software / Libre

ASUS UL30A -- © 2009 David Mentré, license CC-BY-SA I recently installed an Ubuntu Karmic Koala (9.10) Linux distribution on an ASUS UL30A-QX090V laptop. The installation went rather smoothly. You'll find below the useful details.

Despite being in favour of reimbursement of software bundled with hardware, I decided to keep the pre-installed proprietary Windows 7 64 bits. It will allow me to test Windows 7, compare it with my Ubuntu system and test Free Software on Windows.

Under Windows 7: make room for Linux

One needs to make room for the Linux system on the 320 Gb hard disk. Fortunately, Windows is installed in a 74 GB partition and there is one 208 GB empty partition.

So, go to Windows icon -> Computer -> Right-click -> Manage -> Storage -> Disk Management. Three partitions are available:

  • 14,65 GB: no name and not mounted, probably for system re-installation;
  • 74,52 GB (C:) : Windows 7;
  • 208,92 GB (D:) : DATA, empty partition.

One needs to remove DATA partition. Right-click on this partition and choose Remove volume.

If you have a different laptop with no free partition, it might be useful to know that Windows Vista and Windows 7 can resize partitions using the same pre-installed program.

Under my current Ubuntu computer: prepare the USB installation key

I download the ISO image of the latest Ubuntu Karmic Koala 9.10 in 64 bits version: the machine has 4 GB of RAM and you can only access 3 GB with a 32 bits system.

After download, I checked that the MD5 checksum is correct. In a terminal, do "md5sum ubuntu-9.10-desktop-amd64.iso" and search for the result in the UbuntuHashes web page.

I then use usb-creator to setup an USB key with this dowloaded image. Plug in your USB key. Start usb-creator from System -> Administration -> USB Boot Disk Creator. Select the ISO image you have just downloaded and chose the USB key you have just plugged in. Then press Create button. I chose to not use an area where data can be saved on the USB key.

By the way, usb-creator installs what is needed on the USB key and makes it bootable, but it keeps the FAT32 file system so the key can still be used as a regular USB key to share documents.

On the ASUS UL30A-QX090V Laptop: install Ubuntu

Plug in the USB key and power on the laptop.

By pressing F2 when the ASUS logo is displayed, go to the BIOS and configure it to boot on the USB key. The magic trick: the USB key is seen as a hard drive! So you must go to the hard drive boot order sub-menu to put the USB key in first position, before the real hard drive. Save and exit from the BIOS through F10.

The machine then reboots and should boot on the USB key (or do a cold start by powering off then powering on the laptop).

Install Ubuntu as usual. I used the biggest free space, letting Ubuntu chose the partitioning. As this is a laptop, I also chose to encrypt the user's home folder.

After a reboot, you now have a shiny new Linux system on your laptop! Enjoy! :-)

What's working

I haven't tested everything yet. Right now:

  • Working: wired and wireless network (WiFi tested using WPA2), sound output, display at native screen resolution, extended touchpad (emulation of mouse scroll wheel and right-click), processor frequency scaling according to actual use, SDHC card reader;
  • Not tested: sound input, webcam, battery autonomy, 3D acceleration[1], hibernation, external display output (VGA and HDMI);
  • Not woking: nothing yet! ;-)

Notes

[1] But special effects are available on the desktop, so I assume 3D acceleration can be used

11 comments

Thursday, November 26 2009

Organisation : avoir la boite de courrier entrant toujours vide

By d. on Thursday, November 26 2009, 13:00

Panier vide (© 2009 David Mentré - licence CC-BY-SA) Depuis quelques semaines, j'essaye, tant au travail que chez moi, d'avoir ma boite de courrier entrant toujours vide, ou du moins chaque soir.

Je ne sais plus où j'ai lu ce conseil, peut-être dans Get Things Done ou sur un blog. Cette contrainte à un avantage immédiat : se forcer à faire les choses et leur donner une priorité. Avant, bien souvent, je laissais un courriel dans mon dossier entrant pour une tâche ingrate ou quelque chose à-faire-quand-j'aurais-le-temps.[1] Maintenant, puisque ce dossier doit être toujours vide, soit je fais les choses immédiatement ou du moins avant la fin de la journée (le soir avant de partir par exemple), soit je mets le courriel dans un dossier « À faire plus tard » qui, je le sais, ne sera jamais consulté ou très rarement. En d'autres termes, je classifie immédiatement les courriels vraiment important, nécessitant une action immédiate et ceux plus accessoires.

Pour l'instant, cette approche fonctionne. Parfois, j'ai un ou deux courriels que je garde non lu dans ma boite entrante, par ce que je me dis que je n'ai vraiment pas le temps là maintenant et que je dois le faire. Mais si au bout du deuxième jour je n'ai rien fait, je sais que ce courriel n'est pas si important que ça et je le relègue aux oubliettes... ou je fais ce que je dois faire sur ce courriel immédiatement. :-)

Un autre truc que j'utilise, c'est de marquer les actions urgentes ou importantes sur mes courriels en les gardant comme « Non lus ». Comme ça, à chaque fois que je regarde ma boite j'ai l'impression d'avoir du nouveau courrier et je re-regarde les tâches à faire sur ces courriels. C'est pour moi une très bonne incitation à faire les choses.

Et vous, vous avez d'autres trucs pour vous organiser avec le courriel et les autres outils de communication ?

Notes

[1] Temps qu'on n'a jamais, bien évidemment ! :-)

2 comments

Thursday, November 19 2009

OCaml on Ubuntu: looking for a new maintainer

By d. on Thursday, November 19 2009, 13:00 - Free Software / Libre

HELP At some point I helped keeping the OCaml packages on Ubuntu in good shape, especially for the Karmic 9.10 release.

Unfortunately, I have much less free time those days and can no longer monitor OCaml packages on Ubuntu. Is anybody willing to work on this?

The main job is to look at the Debian packages and check if they are currently available in Ubuntu, and rebuild them if necessary. When the OCaml compiler changes (fortunately not so often), one needs to trigger a rebuild of all packages and that can be a bit difficult, mainly because LaunchPad does not provide an interface to rebuild several packages, taking into account their dependencies.

Of course, I would help anybody willing to do that job (explain the needed scripts, issues I had, etc.).

3 comments

Thursday, September 24 2009

Absences...

By d. on Thursday, September 24 2009, 13:00 - Open Street Map

Règle n°23 : ne jamais dire qu'on fera un billet tous les jeudis. Rien que de l'annoncer est suffisant pour ne jamais le faire.

Sinon, le projet dont je parlais dans mon précédent billet a été largement diffusé (avec même un petit article dans SVM), c'est MapOSMatic. C'est un générateur automatique de plans de ville à partir des données libres d'OpenStreetMap. Vous donnez le nom de votre ville est zoouuu vous avez un joli plan avec l'index des rues.

La version actuelle est une première version, on a encore une foule de bugs et de choses à améliorer. Mais les premiers retours sont très positifs : ça fait plaisir ! :-)

Sinon, côté activité libriste sur la région, je suis actif dans plusieurs projets :

Ceci explique peut-être cela. ;-)

Thursday, September 3 2009

C'est la rentrée !

By d. on Thursday, September 3 2009, 13:00 - Free Software / Libre

Helping paw Comme tout le monde, je fais ma rentrée : des tonnes de choses reportées à terminer en urgence et la perspective de nouvelles choses à démarrer.

Côté blog, j'ai décidé de changer sa fréquence avec désormais plus qu'un seul billet par semaine, le jeudi à 13h. Histoire de me laisser un peu de temps pour faire d'autres choses.

Justement, à propos d'autres choses, avec quelques amis on s'est pris une semaine de vacances à coder. Les geeks codeurs comprennent le plaisir qu'on a à faire ce genre de truc. Les autres ont plus de mal. :-) Durant cette semaine on a réalisé un petit projet à partir de zéro. Il ne peut pas encore être diffusé donc je n'en dirais pas plus, si ce n'est qu'il tourne autour d'OpenStreetMap. Stay tuned! ;-)

one comment

Monday, August 3 2009

Août, farniente & Co.

By d. on Monday, August 3 2009, 13:00

Pas de billets en août. Profitez bien de vos vacances (si vous en avez) ou du calme quand les autres sont partis (si vous bossez).

- page 2 of 8 -