[cwn] Attn: Development Editor, Latest Caml Weekly News
Alan Schmitt
alan.schmitt at polytechnique.org
Tue Mar 31 00:42:38 PDT 2009
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
========================================================================
1) First release of focalize, a development environment for high
integrity programs.
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.
========================================================================
2) OSpec - BDD for OCaml
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 :)
========================================================================
3) ocaml cross-compiler
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\*
========================================================================
4) PowerPC 405
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.
========================================================================
5) Google summer of Code proposal
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.
========================================================================
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
(alan.schmitt at polytechnique.org) and I'll mail it to you, or go take a
look at
the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish
to receive it every week by mail, you may subscribe online at
<http://lists.idyll.org/listinfo/caml-news-weekly/> .
========================================================================
--
Alan Schmitt <http://alan.petitepomme.net/>
The hacker: someone who figured things out and made something cool
happen.
.O.
..O
OOO
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20090331/18fb2551/attachment-0001.htm
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 195 bytes
Desc: This is a digitally signed message part
Url : http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20090331/18fb2551/attachment-0001.pgp
More information about the caml-news-weekly
mailing list