[cwn] Attn: Development Editor, Latest Caml Weekly News
Alan Schmitt
alan.schmitt at polytechnique.org
Tue Nov 27 00:39:47 PST 2007
Hello,
Here is the latest Caml Weekly News, for the week of November 20 to
27, 2007.
1) Camlp5 release 5.03
2) Coq Tutorial at POPL 2008: Using Proof Assistants for Programming
Language Research
3) labltk : mini-tutorial
4) ocaml-based magnetism simulation package
5) XmlRpc-Light 0.6
6) Ocaml(opt) & llvm
7) LLVM: A native-code compiler for MiniML in ~100LOC
8) Native-code Smoke demos now for Mac OS X on Intel
========================================================================
1) Camlp5 release 5.03
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
2260d2c1f91dc3c1#99b988e98f8d4d6a>
------------------------------------------------------------------------
** Daniel de Rauglaudre announced:
New release of Camlp5: 5.03
Main changes:
* Added commands mkcamlp5 and mkcamlp5.opt to build camlp5
executables.
* Some small improvements and bug fixes.
For changes of all versions, see file CHANGES in Camlp5 site.
Download the sources and the documentation at:
<http://pauillac.inria.fr/~ddr/camlp5/>
** David Teller asked and Daniel de Rauglaudre answered:
> By quickly browsing the documentation, I haven't been able to
understand
> the core of the difference between camlp4 and camlp5. I mean,
there's a
> Pcaml module which seems to have disappared from camlp4 in 3.10,
but I
> assume that's not where it ends. Could you tell us a bit more
about it ?
Camlp5 is the continuation of the classical Camlp4.
At OCaml 3.10, Camlp4 was changed, with some incompatible features,
sometimes implying many changes in user programs. A solution is to
use Camlp5. Some softwares, e.g. "Coq", adopted this solution.
** Richard Jones also answered:
Camlp4 was extensively changed for the 3.10 release, in many ways not
for the better (it's much bigger now for a start, and not backwards
compatible, and has almost no documentation, and I have problems with
it and findlib).
Camlp5 is the camlp4 from 3.09.3 (before the changes / fork), and with
some ongoing maintenance.
3.09 3.10
-------+----/\/----+---------> "new" camlp4 (distributed with OCaml)
|
\
--------------------> camlp5 (now distributed separately)
If you had a package which depends on camlp4 in 3.09.3, you need to
modify it so it compiles with OCaml 3.10. An alternative which
doesn't involve modifying your package is to install camlp5. You can
install both in parallel no problem.
Debian ships both. Fedora will soon as well.
========================================================================
2) Coq Tutorial at POPL 2008: Using Proof Assistants for Programming
Language Research
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
f85425f2099921d3#dc2694c20eafb6b0>
------------------------------------------------------------------------
** Stephanie Weirich announced:
Tutorial Announcement and Call for Participation
Using Proof Assistants for Programming Language Research
Or:
How to Write Your Next POPL Paper in Coq
San Francisco, CA, 8 Jan 2008
Co-located with POPL 2008
Sponsored by ACM SIGPLAN
<http://plclub.org/popl08-tutorial/>
=======================================================================
The University of Pennsylvania PLClub invites you to participate in a
tutorial on using the Coq proof assistant to formalize programming
language
metatheory.
This tutorial will be tailored to people who are familiar with syntactic
proofs of programming language metatheory (type soundness, etc.), but
have
never used a proof assistant. At the end of the day, participants
will have
a reading knowledge of Coq and a running start on using Coq in their own
work.
This tutorial will be hands-on, with breaks for exercises;
participants are
strongly encouraged to bring a laptop running Coq 8.1 (or a later
release)
and either Proof General or CoqIDE.
Tutorial topics
- Defining language semantics in Coq
- Abstract syntax
- Inductively-defined relations
- Derivations
- Proving simple results
- Fundamental tactics
- Automation
- Forward and backward reasoning
- Scaling up to POPLmark
- Semantic functions and conversion
- Sets and environments
- Representing binding
- Locally nameless representation
- Freshness through cofinite quantification
- Syntactic type soundness
Registration will be through the POPL 2008 registration site:
<http://www.regmaster.com/conf/popl2008.html>
The tutorial is organized and presented by members of the University of
Pennsylvania PLClub: Brian Aydemir, Aaron Bohannon, Benjamin Pierce,
Jeffrey
Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic.
Questions can be sent to Stephanie Weirich (sweirich at cis.upenn.edu).
========================================================================
3) labltk : mini-tutorial
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
fbfe88f193572aa8#3ac9d5e0e18ab0c9>
------------------------------------------------------------------------
** François Thomasset announced:
As I could not find easily informations on the use of labltk, I took
a PerlTk
tutorial with nice pedagogic qualities, and adapted it to labltk:
<http://www-rocq.inria.fr/~thomasse/Labltk/Tutoriel_FT/>
I know this is still far from being a complete tutorial: a number of
features
are not described, explanations are a bit terse. I may try to improve
it some
day. Meanwhile I hope this batch of examples can be useful to other
people than
myself. Please warn me about any mistakes or imprecision.
========================================================================
4) ocaml-based magnetism simulation package
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
5293f5244e787a94#70cfd4be024478bd>
------------------------------------------------------------------------
** Thomas Fischbacher announced:
I thought I should mention this to keep people informed about
large projects done in OCaml.
Micromagnetism is a rather hot topic these days. There are
a number of packages around that allow one to do physical
simulations of sub-micron scale magnetic systems, but there
is one around (ours) which is written mostly in ocaml.
(The user interface is python, though.)
The rationale for using ocaml was that we needed both speed
and enough flexibility to do symbolic manipulations.
Actually, this micromagnetism package is just a library on
top of a much more generic multiphysics simulation system
that was designed to deal with a very broad class of
generalized reaction-diffusion systems, whose ultimate goal
is to automatically compile an abstract problem specification
(containing differential operators and equations of motion
in symbolic form) down to some numerical finite element code.
The first beta-release (still a bit wobbly) is at:
<http://nmag.soton.ac.uk>
** Andrej Bauer asked and Thomas Fischbacher answered:
> I have suspected for a while that writing the computational part in
> ocaml and the user interface in python is a good combination. What is
> your experience? Are there any drawbacks? Would you do it again?
We use a modified variant of Art (arty) Yerkes' old "pycaml" module.
Essentially, I had to re-write quite a bit of it, as both reference
counting on the Python side and Gc management on the OCaml side were
broken. One impotant issue is that the pycaml module (which also is
part of Debian) does not recognize properly that python library
primitives often differ in their behaviour concerning whether they
increase the reference count of a return value or not.
Also, we added a lot of extra stuff and goodies which allows us to
interface ML to python quite smoothly. When I call a ML-function from
python, dynamic type-checking of all the arguments is automatic and
generates appropriate python exceptions. Here is an example for a
python-wrapped ML function that uses our extended pycaml module:
let _py_raw_cvode_advance =
python_pre_interfaced_function
[|CamlpillType; (* the cvode *)
CamlpillType; (* the result vector *)
FloatType; (* target time *)
IntType; (* max nr_steps, -1 for "no limit" *)
|]
(fun args ->
let cvode = cvode_from_ocamlpill args.(0) in
let FEM_field (_,_,v_result) = field_from_ocamlpill args.(1) in
let target_time = pyfloat_asdouble args.(2) in
let max_steps = pyint_asint args.(3) in
let result_time =
Sundials.cvode_advance cvode target_time v_result max_steps
in
pyfloat_fromdouble result_time)
;;
It is nice to be able to implement other high-level python/caml
interface abstractions through functional tricks -- such as a caml
function constructing and accessing a higher-rank nested-list python
tensor.
How does it feel? If I had a need for some specific fast low-level
extension to python, I would prefer using python+ocaml a thousand
times over python+C. It is just so much nicer not having to worry
about reference counting issues. Even if you feel you can do it
right, there is always a bit of doubt. Doubly so if you are not
the sole developer. I would not let our PhD students write C
extensions to python, but I have no problems whatsoever letting
them extend python via ocaml functions.
One sort-of limitation is that we use our own python interpreter.
(I.e. the main program is written in OCaml and eventually provides
a python prompt or runs a python script.)
This is necessary in our situation as we also want to support running
in parallel under MPI control, and the MPI libraries do some nasty
arg-passing things that upset an unmodified python interpreter. So, we
do not load some object-code module containing all the ML runtime
environment system into a standard python interpreter; technically, that
should be possible as well on many platforms, but it is not relevant in
our particular case here.
On the other hand, of course, if one can completely avoid such
inter-language interfaces, the better. In principle, both Python
and OCaml are widely loved because of flexibility they both derive
from LISP. So, some situations, one may be better off using e.g. the
Gambit Scheme Compiler instead (which has, by the way, a terrific
C interface!)
It depends a lot on your constraints. If you want to build something
that can be easily integrated with lots of data processing libraries
that are readily available and accessible to casual programmers
(engineers, physicists, etc.), providing python support seems to be a
very good choice to me. It is rather popular among engineers these
days, which I consider mostly a good thing.
Also, if you want your PhD students to be productive at writing code
that has to run fast, and if they are spoilt enough from previous
exposure to imperative languages that you cannot really teach them
Lisp/Scheme within a short amount of time ;-), then ocaml certainly
is a very good choice. (In terms of what we teach our students about
caml, this is not much more than the core ML language plus a bit
about the C interface. They usually pick that up in less than 3 months.
With C++, they never could be productive after such a short amount
of time.)
So, I would say: in an ideal computing world, we would all be expert
Scheme hackers, but in the real world, python+ocaml can be an extremely
productive and powerful combination. I have used and combined many
systems in the past, but I would have difficulty naming anything
else I played with that appeared even remotely as powerful.
I know that in the longer run, we certainly should split nmag and
ship our new and improved pycaml module separately (after brushing
it up a bit) -- and a few other modules as well. But for now,
we are busy dealing with other issues. (We are, after all,
physicists studying real physical systems, so all this symbolic
mumbo-jumbo in nmag/nsim is just a tool to us.)
========================================================================
5) XmlRpc-Light 0.6
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
9fbd8b6b789533cb#52277cf02782bc2c>
------------------------------------------------------------------------
** Dave Benjamin announced:
I have released XmlRpc-Light 0.6. XmlRpc-Light is an XmlRpc client and
server library written in OCaml. It requires Xml-Light and Ocamlnet 2.
<http://code.google.com/p/xmlrpc-light/>
This release introduces a new module, XmlRpcDateTime, which provides a
date time type (still a tuple of integers), time-zone-aware equality and
comparison, XmlRpc-flavored iso-8601 parsing and generation, time zone
adjustment, and conversion functions to- and from- Unix float and
Unix.tm for both local and UTC times. There is also a handy "now()"
function to build a time stamp for the current time. The Unix conversion
functions follow the same naming convention as Julien Signoles' calendar
library to ease integration with that package.
I have written a suite of unit tests, based on Maas-Maarten Zeeman's
oUnit framework, which you can run by typing "make test". These tests
cover parsing and generation of XmlRpc values and messages, date-time
parsing and arithmetic, and the server's function call and error
handling behavior.
The WordPress example library has been updated to support WordPress 2.3,
which now provides UTC date-time values. The interface has been kept
mostly the same. It now uses XmlRpcDateTime.t instead of defining a
"datetime" type, but this shouldn't break any code since due to
structural typing. The one thing that doesn't work the same is the
"suggest_categories" method, since WordPress has completely changed the
structure of its results. Rather than attempt to make any sense of the
new result format, which is rather odd, I decided to punt here and just
return an XmlRpc.value (variant).
Finally, I have added support for the somewhat controversial "nil" type.
Not all servers support this type, and Dave Winer has been known to be
adamantly opposed to it, but it has become a de-facto standard and quite
a few XmlRpc libraries support it now. If you don't like it, don't use
it. =)
========================================================================
6) Ocaml(opt) & llvm
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
1c777227f8efb204#2b201480b60a879d>
------------------------------------------------------------------------
** Basile STARYNKEVITCH said:
As some might probably know, the LLVM compiler <http://llvm.org/> has
(at
least in its latest SVN snapshot) a binding for Ocaml. This means that
one could code in Ocaml some stuff (eg a JIT-ing compiler) which uses
(and links with) LLVM libraries.
<http://lists.cs.uiuc.edu/pipermail/llvmdev/2007-November/011481.html>
<http://lists.cs.uiuc.edu/pipermail/llvmdev/2007-November/011507.html>
However, to generate code with LLVM for Ocamlopt, this is not enough,
since while LLVM does have hooks to support garbage collection
<http://www.llvm.org/docs/GarbageCollection.html>
I don't know of any actual hooks to fit into the needs of Ocamlopt
garbage colector (which AFAIK require some specific frame descriptors in
the code, in some hashtables, which details are tricky and known to very
few implementors, perhaps only Xavier Leroy & Damien Doligez).
So is there any code to fit the Ocaml GC requirements into LLVM
abilities, ie to use LLVM to generate (eg JIT) code which respect Ocaml
GC requirements.
Of course, I do know that there are some typing issues and theoritical
points which I deliberately ignore here. I'm supposing the guy wanting
to LLVM for Ocaml is knowing that he seeks trouble.
And Metaocaml is (unfortunately) nearly dead: future (in ocaml 3.11 or
3.12) dynamic libraries ability is not a full replacement! Even if one
might generate Ocaml code and compile & dlopen it in a future version of
Ocaml.
** Gordon Henriksen then said:
To avoid cross-posting, my followups to this thread will be on llvmdev.
<http://lists.cs.uiuc.edu/pipermail/llvmdev/2007-November/011527.html>
========================================================================
7) LLVM: A native-code compiler for MiniML in ~100LOC
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
8ba2204855fc5e46#5aee553df34548e2>
------------------------------------------------------------------------
** Jon Harrop announced:
I recently rediscovered the Low-Level Virtual Machine (LLVM) project
that has
since been adopted by Apple:
<http://llvm.org>
This is a library (with OCaml bindings!) that allows you to write a
compiler
that generates their RISC-like intermediate language (IL) that can
then be
compiled to native code. LLVM even supports JIT compilation.
I went through the usual steps in trying this and was extremely
impressed with
the results. After only two days I was able to create an optimizing
native-code compiler for a subset of CAML large enough to represent the
following Fibonacci program:
let rec fib n =
if n <= 2 then 1 else
fib(n-1) + fib(n-2)
do fib 40
The compiler is written entirely in OCaml, using camlp4 for lexing and
parsing, and the whole thing is only ~100 lines of code!
I'll detail exactly how you can use LLVM from OCaml in a future OCaml
Journal
article:
<http://www.ffconsultancy.com/products/ocaml_journal/?ol>
Meanwhile here's my latest source:
type expr =
| Int of int
| Var of string
| BinOp of [ `Add | `Sub | `Leq ] * expr * expr
| If of expr * expr * expr
| Apply of expr * expr
type defn =
| LetRec of string * string * expr
open Camlp4.PreCast
let expr = Gram.Entry.mk "expr"
let defn = Gram.Entry.mk "defn"
let prog = Gram.Entry.mk "prog"
EXTEND Gram
expr:
[ [ "if"; p = expr; "then"; t = expr; "else"; f = expr ->
If(p, t, f) ]
| [ e1 = expr; "<="; e2 = expr -> BinOp(`Leq, e1, e2) ]
| [ e1 = expr; "+"; e2 = expr -> BinOp(`Add, e1, e2)
| e1 = expr; "-"; e2 = expr -> BinOp(`Sub, e1, e2) ]
| [ f = expr; x = expr -> Apply(f, x) ]
| [ v = LIDENT -> Var v
| n = INT -> Int(int_of_string n)
| "("; e = expr; ")" -> e ] ];
defn:
[ [ "let"; "rec"; f = LIDENT; x = LIDENT; "="; body = expr ->
LetRec(f, x, body) ] ];
prog:
[ [ defns = LIST0 defn; "do"; run = expr -> defns, run ] ];
END
open Printf
let program, run =
try Gram.parse prog Loc.ghost (Stream.of_channel stdin) with
| Loc.Exc_located(loc, e) ->
printf "%s at line %d\n" (Printexc.to_string e)
(Loc.start_line loc);
exit 1
open Llvm
let ty = i64_type
let ( |> ) x f = f x
type state =
{ fn: llvalue;
blk: llbasicblock;
vars: (string * llvalue) list }
let bb state = builder_at_end state.blk
let new_block state name = append_block name state.fn
let find state v =
try List.assoc v state.vars with Not_found ->
eprintf "Unknown variable %s\n" v;
raise Not_found
let cont (v, state) dest_blk =
build_br dest_blk (bb state) |> ignore;
v, state
let rec expr state = function
| Int n -> const_int ty n, state
| Var x -> find state x, state
| BinOp(op, f, g) ->
let f, state = expr state f in
let g, state = expr state g in
let build, name = match op with
| `Add -> build_add, "add"
| `Sub -> build_sub, "sub"
| `Leq -> build_icmp Icmp_sle, "leq" in
build f g name (bb state), state
| If(p, t, f) ->
let t_blk = new_block state "pass" in
let f_blk = new_block state "fail" in
let k_blk = new_block state "cont" in
let cond, state = expr state p in
build_cond_br cond t_blk f_blk (bb state) |> ignore;
let t, state = cont (expr { state with blk = t_blk } t) k_blk in
let f, state = cont (expr { state with blk = f_blk } f) k_blk in
build_phi [t, t_blk; f, f_blk] "join" (bb state), state
| Apply(f, arg) ->
let f, state = expr state f in
let arg, state = expr state arg in
build_call f [|arg|] "apply" (bb state), state
let defn m vars = function
| LetRec(f, arg, body) ->
let ty = function_type ty [| ty |] in
let fn = define_function f ty m in
let vars' = (arg, param fn 0) :: (f, fn) :: vars in
let body, state =
expr { fn = fn; blk = entry_block fn; vars = vars' } body in
build_ret body (bb state) |> ignore;
(f, fn) :: vars
let int n = const_int ty n
let main filename =
let m = create_module filename in
let string = pointer_type i8_type in
let print =
declare_function "printf" (var_arg_function_type ty [|string|])
m in
let main = define_function "main" (function_type ty [| |]) m in
let blk = entry_block main in
let bb = builder_at_end blk in
let str s = define_global "buf" (const_stringz s) m in
let int_spec = build_gep (str "%d\n") [| int 0; int 0 |]
"int_spec" bb in
let vars = List.fold_left (defn m) [] program in
let n, _ = expr { fn = main; blk = blk; vars = vars } run in
build_call print [| int_spec; n |] "" bb |> ignore;
build_ret (int 0) bb |> ignore;
if not (Llvm_bitwriter.write_bitcode_file m filename) then exit 1;
dispose_module m
let () = match Sys.argv with
| [|_; filename|] -> main filename
| _ as a -> Printf.eprintf "Usage: %s <file>\n" a.(0)
To use it, simply download and install the latest SVN version of LLVM
(which
even builds and installs the OCaml bindings for you!) and then do:
$ ocamlc -g -dtypes -pp camlp4oof -I +camlp4 dynlink.cma
camlp4lib.cma -cc g++
llvm.cma llvm_bitwriter.cma minml.ml -o minml
$ ./minml run.bc <fib.ml
$ llc -f run.bc -o run.s
$ gcc run.s -o run
$ ./run
102334155
$
You can look at the generated intermediate representation with:
$ llvm-dis -f run.bc
$ cat run.ll
If anyone improves upon this I'd love to hear about it! :-)
========================================================================
8) Native-code Smoke demos now for Mac OS X on Intel
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/
4f8c5ef33e53a7b0#2264589aa36e105f>
------------------------------------------------------------------------
** Jon Harrop announced:
We just updated the Smoke vector graphics pages with native Mac OS X
executables of all three demos:
<http://www.ffconsultancy.com/products/smoke_vector_graphics/?ol>
We'll be adding more demos and functionality to this library
(including the
free bytecode edition) in the new year.
========================================================================
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 --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 186 bytes
Desc: This is a digitally signed message part
Url : http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20071127/d716462a/attachment.pgp
More information about the caml-news-weekly
mailing list