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