Here is the latest Caml Weekly News, for the week of March 24 to 31, 2009.
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/c69ec89f1a928509#Pierre Weis announced:
Hi to all of you careful bug hunters and happy hackers reading this message! It is my pleasure to announce the first public release for FoCaLize, a purely functional language and environment to express and formally prove algorithms and their implementation. (0) What is it ? ---------------- FoCaLize is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLize provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of those properties from within the program source code. The FoCaLize compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator that produces in turn the Coq proof terms that are formally verified. The FoCaLize compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developped in FoCaLize can be efficiently compiled to native code on a large variety of architectures. Last but not least, FoCaLize automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance. The FoCaLize system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation, while proving that such an implementation meets its specification or design requirements. The FoCaLize language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically done relies on Coq formal proof verification. FoCaLize is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantics, featuring a rock-solid infrastructure and greatly improved capabilities. (1) Where to find it ? ---------------------- FoCaLize home page is http://FoCaLize.inria.fr/ FoCaLize source files can be found at http://FoCaLize.inria.fr/download/focalize-0.1.0.tgz (2) How to install it ? ----------------------- Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.1.0 and follow the simple instructions written there.
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/13b63aa5afc13a61#Andre Nathan announced:
I would like to announce the availability of OSpec, an RSpec-inspired Behavior-Driven Development library for OCaml using a Camlp4 syntax extension. It is available at http://github.com/andrenth/ospec/tree/master Here's a simple example of OSpec's syntax: describe "An even number" do it "should be divisible by two" do let divisible_by_two x = x mod 2 = 0 in 42 should be divisible_by_two done; (* or simply: *) it "should be divisible by two" do (42 mod 2) should = 0 done done I must say that this is the first time I use Camlp4 (in fact I started writing this to learn about it), so there are probably better ways to accomplish the functionality that OSpec provides. The code is horrible and it will make your eyes bleed. However, since there was a question about the availability of such a library recently on the list, I decided to make it public. Maybe I can get some contributions to this :)
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/c8b919211170f402#Joel Reymont asked and Richard Jones replied:
> Is there a ready-made Fedora package for the OCaml cross-compiler? Note that we _only_ support Fedora Rawhide (the development version of OCaml) and future Fedora 11 and above. To find out about Rawhide, see: http://fedoraproject.org/wiki/Releases/Rawhide If you have F-10, I believe that you can upgrade it to Rawhide simply by editing a file in /etc/yum.repos.d. But ask about that on the main Fedora mailing lists since I'm not sure. Anyway, to install the cross-compiler, create a new file /etc/yum.repos.d/mingw.repo which contains: [mingw] name=Fedora Windows cross-compiler, libraries and tools baseurl=http://homes.merjis.com/~rich/mingw/fedora-10/x86_64/ enabled=1 gpgcheck=0 Note that you will need to adjust the baseurl to match your version of Fedora and architecture. Then do: # yum install mingw32-ocaml Actually there are several packages you can install. Poke around http://homes.merjis.com/~rich/mingw/ to see which ones. I would like to cross-compile a GTK+ app but can't find instructions. To cross-compile an OCaml program I strongly suggest that you start off with the example package that I created / used for the OCaml Users Conference talk last month: http://www.annexia.org/tmp/ocaml-mingw-gtk/ Please join the mailing list and ask questions there so we can share the knowledge: https://admin.fedoraproject.org/mailman/listinfo/fedora-mingw Any OCaml + lablgtk2 program should be straightforward to cross-compile for Windows. Mostly difficulties will arise only if the program uses some weird libraries.Richard Jones later corrected:
[Too late at night to be posting ..] > Note that we _only_ support Fedora Rawhide (the development version of > OCaml) ^Fedora > baseurl=http://homes.merjis.com/~rich/mingw/fedora-10/x86_64/ That baseurl should be: baseurl=http://homes.merjis.com/~rich/mingw/fedora-rawhide/x86_64/ Replace x86_64 with i386 as appropriate. If you have another architecture then you will have to rebuild the compiler from the source RPMs. > # yum install mingw32-ocaml Even better is: # yum install mingw32-ocaml\*
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/9f2d3beb16ac9e17#Gregory Bellier asked and Basile STARYNKEVITCH replied:
> Do you know if it is possible to compile caml code on a PowerPC 405 > from the Vertex 4 family ? > We'd like to put this processor in a FPGA. > On the Caml's website, it is written "PowerPC" but is it only for > Macintosch ? That is probably not so hard if your processor runs some Linux kernel, or if you want to run only ocaml bytecode (not native). The point is in what kind of runtime environment will your Ocaml run? Also, what is your development toolchain? Are executables in ELF format? ... What is your knowledge of Ocaml internals (notably the stdlib, the runtime C API)? Do you have a usual C lib?Gregory Bellier then said and Basile STARYNKEVITCH replied:
> Yes, it will run Linux. It will have the uclibC or even the lib C. > The best case is to run native code for better performance. We'd like > to cross-compile for the PowerPC. > I'm not a FPGA expert, I'm asking questions for a colleague who works > on it. > From what you're saying, it should work properly because of the > non-exotic environment thanks to Linux. Am I correct ? Probably yes. A few years ago, I had a Powerbook G4 with a 32 bits PowerPC running Linux, and Ocaml did compile and run fine, even in native mode. Of course, I understand that your ocaml code runs inside an application in linux user mode (not inside the kernel!). I would expect you might have minor issues in configuration or whatsover. I suppose you have enough RAM (and I have no idea what that means exactly on your system). Please publish the patches you'll need to implement your solution. But I never tried all that, so take all my saying with a big grain of salt. BTW, I'm curious: what kind of embedded application do you want to code in Ocaml for what sort of device or system?Xavier Leroy then said:
Just to complement Basile's excellent answers: > Do you know if it is possible to compile caml code on a PowerPC 405 > from the Vertex 4 family ? > We'd like to put this processor in a FPGA. On the Caml's website, > it is written "PowerPC" but is it only for Macintosch ? Not just Macintosh: PowerPC/Linux is also supported and works very well. > Yes, it will run Linux. It will have the uclibC or even the lib C. Then you're in good shape. I would expect a basic OCaml system to work with uclibC, although a number of external libraries might not. With GNU libC, everything will work but watch out for code size: glibc is big! > The best case is to run native code for better performance. We'd > like to cross-compile for the PowerPC. Setting up OCaml as a cross-compiler is a bit of a challenge at the moment. As a prerequisite, you'll need a complete cross-compilation environment for C: cross-compiler, cross-binutils, libraries and header files for your target. It sounds obvious but in my experience that's quite hard to get right. Then, there is a bit of configuration magic to be done on the OCaml side. Write back for help if you're going to follow this way. A perhaps simpler alternative would be to compile on a bigger PowerPC/Linux platform. An old Mac would be handy for this, but you can also use a Sony Playstation 3 (if you happen to have one around for, ahem, R&D purposes) after installing YellowDog Linux on it.Xavier Clerc then added:
I have built a MacOS-to-Linux cross-compiler last week. I do confirm that the hard part is getting a cross-[g]cc up and running. In fact, this is so tedious that I strongly encourage to resort to either a prepackaged cross-[g]cc (from binaries, from a Linux packaging system, whatever), or to the excellent "crosstool" available at : http://www.kegel.com/crosstool/ On the OCaml side, there are very few things to do and they are quite straightforward. First, you have to emulate the behaviour of "./configure" by producing "config/m.h", "config/s.h", and "config/ Makefile" by hand. This is easier than it may sound, just start from "config/m- templ.h", "config/s-temp.h", and "config/Makefile-templ" (these are comprehensively commented). Then, you will have to slightly patch some Makefiles, and you are done. I will setup a webpage with all the necessary steps and patches as soon as I get my notes organized. This will allow us to share knowledge on the subject.
Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/3249f410fe061579#Continuing the thread from last week, Xavier Leroy replied to Jon Harrop:
> Is MLton not several times faster than OCaml for symbolic computing? No, only in your dreams. If there was a Caml or SML compiler that was twice as fast as Caml on codes like Coq or Isabelle/HOL, everyone (me included) would have switched to that compiler a long time ago. MLton can probably outperform Caml on some symbolic codes, but not by a large factor and not because of data representation strategies (but rather because of more aggressive inlining and the like).Joel Reymont said and Jon Harrop replied:
> There's a nice discussion of LLVM in the context of Alice ML here: > > http://lambda-the-ultimate.org/node/440 > > I'm told that not much has changed since. Whoever told you that was wrong: a lot has changed in LLVM over the past five years. Indeed, it is one of the most rapidly advancing open source projects in existence thanks to extensive contributions from the likes of Apple and Google. LLVM has long since had full support for tail calls. See the "tco" example in the "test.ml" file of HLVM for an example. I tested tail calls in LLVM extensively before choosing to build upon it. I have found and worked around some minor bugs in their TCO implementation but Arnold Schwaighofer just committed a fix that will be in LLVM 2.6. The toy Scheme implementation that was in LLVM five years ago has long since been overshadowed by full-blown FPL implementations like the Pure language: http://pure-lang.sourceforge.net/ I don't understand Anton van Straaten's other complaint about the lack of closures. They are trivial to implement. Again, look at the examples in HLVM (although they are hand-coded because we don't have lambda lifting yet). Moreover, LLVM offers huge advantages: .. LLVM-generated code on x86 is often several times faster and can be up to an order of magnitude faster than any existing FPL implementation. Moreover, LLVM can JIT compile, making it trivial to outperform interpreted languages like OCaml's current top-level. See HLVM's preliminary performance results, for example: http://flyingfrogblog.blogspot.com/2009/03/performance-ocaml-vs-hlvm-beta-04.html .. LLVM generates code very quickly, rivalling ocamlopt's compile times. .. SSE and atomic instructions for high-performance numerics and parallelism/concurrency. .. Mature and easy-to-use API with native OCaml bindings. .. Substantial friendly community who not only explain things but fix them for you quickly. .. Commercially viable: LLVM is already shipping in products. LLVM does have some disadvantages: .. LLVM's JIT compiler is not multicore capable (but what FPL implementations are?). .. LLVM does not bundle a reusable high-performance concurrent garbage collector (but what standalone FPLs do?). .. LLVM's GC API is experimental so if you want a specialized run-time (e.g. optimized specifically for symbolics) you have to write it yourself.Xavier Leroy said and Jon Harrop replied:
> "But shadow stacks are the only way to go for GC interface!" > No, it's probably the worst approach performance-wise; even a > conservative GC should work better. I blogged a quick analysis of the performance of HLVM's current shadow stack code: http://flyingfrogblog.blogspot.com/2009/03/current-shadow-stack-overheads-in-hlvm.html There is a lot of scope for optimization but these results were enlightening to show where the effort should be put. In particular, shadow stack updates by the mutator (and not the collector, as I had incorrectly assumed) account for the entire performance difference between OCaml and HLVM on the 10-queens benchmark.
Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).
If you know of a better way, please let me know.
If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.
If you also wish to receive it every week by mail, you may subscribe online.