Hello

Here is the latest Caml Weekly News, for the week of March 24 to 31, 2009.

1. First release of focalize, a development environment for high integrity programs.
2. OSpec - BDD for OCaml
3. ocaml cross-compiler
4. PowerPC 405
5. Google summer of Code proposal

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/c69ec89f1a928509#

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#

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#

> 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.
			

[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#

> 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?
			

> 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?
			

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. 
			

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#

> 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).
			

> 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.
			

> "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.
			

Using folding to read the cwn in vim 6+

Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).

:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1
zM

If you know of a better way, please let me know.

Old cwn

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.

Alan Schmitt