Caml Weekly News Previous week Up Next week

Hello

Here is the latest Caml Weekly News, for the week of October 24 to November 07, 2006.

  1. dypgen : bug fixed and new manual
  2. macosx, ocaml, findlib and extlib
  3. Binary RPMs of OCaml 3.09.3 for Fedora 2-6 and Red Hat Enterprise Linux 4 are available.
  4. Olmar - almost a C++ parser for Ocaml
  5. Bedwyr 1.0
  6. Printing of types
  7. gettext for caml
  8. Ocamlp3l
  9. Post-docs on formal compiler verification
  10. Oracle OCCI C++ interface

dypgen : bug fixed and new manual

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/50f0f95cc75b1705/e093fcdbd1e9bb6f#e093fcdbd1e9bb6f

Emmanuel Onzon announced:
A new version of dypgen is available at 
http://perso.ens-lyon.fr/emmanuel.onzon/ 

It fixes bugs with merge functions and with the files 
testdyn1.tiny and testdyn2.tiny. 
The manual has been completed with examples and more details.
			

macosx, ocaml, findlib and extlib

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/1a49c6168215c0d7/a00d69b76765958d#a00d69b76765958d

Later in this thread, Pietro Abate announced:
I've created two Mac packages for extlib and findlib and I've submitted 
patches respectively against extlib-1.5 and findlib-1.1.2pl1.  As far as 
I 
can see, these packages play well with the mac package of the ocaml 
toolchain 
from inria. 
For those who are interested, you can get patches and packages here. 
http://users.rsise.anu.edu.au/~abate/macosx/ 
It would be great if these packages could be hosted somewhere more 
official 
(hint hint :)) 
I haven't tested them very carefully ... so please let me know if I've 
done 
something silly...
			

Binary RPMs of OCaml 3.09.3 for Fedora 2-6 and Red Hat Enterprise Linux 4 are available.

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/1eabdb2bc45af369/4670f52ead6095c0

Aleksey Nogin announced:
I've built binary RPMs (Red Hat packages) of OCaml 3.09.3 for Fedora 2, 
3, 4, 5, and 6 and for Red Hat Enterprise Linux 4. Download them from 
http://rpm.nogin.org/ocaml.html
			

Olmar - almost a C++ parser for Ocaml

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/19b0829e1815f9bd/ad2a8d163c2020b8#ad2a8d163c2020b8

Hendrik Tews announced:
I would like to announce a new snapshot release of 

   Olmar -- a system to process C++ programs in Ocaml 

available from http://www.cs.ru.nl/~tews/olmar/ 

New in this release: 

- syntax trees are much larger: All xml annotated fields are 
  available in Ocaml. This includes, for instance, an (elsa 
  computed) type for all expressions. 

General description: 

Olmar is a patch for the Elkhound/Elsa [1] C/C++ parser that 
permits the Elsa parser to translate its internal abstract syntax 
tree into an Ocaml value, which can then be further processed by 
an Ocaml program. 

Olmar comes with ast_graph, a tool that can dump the abstract 
syntax tree in the dot language. You can therefore now admire the 
syntax tree of Ocaml's minor garbage collector at 
http://www.cs.ru.nl/~tews/olmar/minor_gc.ps.gz 

License: BSD (following Elsa/Elkhound) 

[1] http://www.cs.berkeley.edu/~smcpeak/elkhound/
			

Bedwyr 1.0

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/6ddbf4b90652a933/9ee433f648f06922#9ee433f648f06922

David Baelde announced:
We would like to announce the first release of a new system written in 
OCaml. Bedwyr is an extended logic programming language that allows 
model-checking directly on syntactic expressions possibly containing 
bindings. 

We believe that it's an interesting tool for computer scientists, as 
it allows simple reasoning on declarative specifications, with several 
good examples, notably bisimulation checking for the pi-calculus. 
Other examples include type systems, games, logics, etc. 

But another interest for the caml-list readers might be the re-usable 
core components of Bedwyr, notably higher-order pattern unification 
and term indexing. Although we don't distribute these separately, I'd 
be happy to do so if anybody is interested. 

You will find a general description of Bedwyr below this message. 
More details can be found on Bedwyr website: 
 http://slimmer.gforge.inria.fr/bedwyr/ 

Sincerely, 

Bedwyr developers 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

                              Bedwyr 
            A proof-search approach to model checking 
              http://slimmer.gforge.inria.fr/bedwyr/ 

Bedwyr is a programming framework written in OCaml that facilitates 
natural and perspicuous presentations of rule oriented computations 
over syntactic expressions and that is capable of model checking based 
reasoning over such descriptions. 

Bedwyr is in spirit a generalization of logic programming. However, it 
embodies two important recent observations about proof search: 

 (1) It is possible to formalize both finite success and finite failure 
   in a sequent calculus; proof search in such a proof system can 
   capture both may and must behavior in operational semantics 
   specifications. 

 (2) Higher-order abstract syntax can be supported at a logical level 
   by using term-level lambda-binders, the nabla-quantifier, 
   higher-order pattern unification, and explicit substitutions; 
   these features allow reasoning directly on expressions containing 
   bound variables. 

The distribution of Bedwyr includes illustrative applications 
to the finite pi-calculus (operational semantics, bisimulation, 
trace analyses and modal logics), the spi-calculus (operational 
semantics), value-passing CCS, the lambda-calculus, winning strategies 
for games, and various other model checking problems. These examples 
should also show the ease with which a new rule-based system and 
particular questions about its properties can be be programmed in 
Bedwyr. Because of this characteristic, we believe that the system can 
be of use to people interested in the broad area of reasoning about 
computer systems. 

The present distribution of Bedwyr has been developed by the following 
individuals: 

 David Baelde & Dale Miller (INRIA & LIX/Ecole Polytechnique) 
 Andrew Gacek & Gopalan Nadathur (University of Minneapolis) 
 Alwen Tiu (Australian National University and NICTA). 

In the spirit of an open-source project, we welcome 
contributions in the form of example applications and also new 
features from others.
			

Printing of types

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/f0a7d593ce81bee2/7a4bbd3e587d9538#7a4bbd3e587d9538

Jacques Carette asked:
When looking at inferred types in the presence of modules and 
combinations of abstract and concrete types, the results are often quite 
puzzling.  For small pieces of code, it is not a big issue.  When one is 
using 4th-order functors (!), with a mixture of abstract and concrete 
types, a fair amount of type synonyms, error message become extremely 
difficult to interpret! 
Below is some (largish for an email) code that demonstrates this.  It 
seems difficult to show how puzzling this gets with much smaller code, 
although one can indeed reproduce the behaviour with smaller code.   
Consider first 
module Sig = struct 
  type domain_is_field 
  type domain_is_ring 
  module type DOMAIN = sig 
    type kind 
    type v 
    val z : v 
  end 
  module type COLL = sig 
    module Dom : DOMAIN 
    type coll 
  end 
end 

module Doms = struct 
  open Sig 
  module FDomain = struct 
    type kind = domain_is_field 
    type v = float 
    let z = 0.0 
  end 
  module IDomain = struct 
    type kind = domain_is_ring 
    type v = int 
    let z = 0 
  end 
  module GColl(Dom:DOMAIN) = 
    struct 
      module Dom = Dom 
      type coll = Dom.v list 
    end 
end ;; 

In the above, the printed types all seem quite reasonable. 
Now we start with some more complex stuff: 
module GEF = struct 
  open Sig 
  module DivisionUpdate 
      (C:COLL with type Dom.kind = domain_is_field) = struct 
    let update x = x 
  end 
  module Gen(C: COLL) 
      (Update: functor(C:COLL with type Dom.kind = C.Dom.kind) 
               -> sig val update : C.Dom.v -> C.Dom.v end) = 
    struct 
      module U = Update(C) 
      let foo = U.update(C.Dom.z) 
    end 
end;; 

where the printed type is 
#                             module GEF : 
  sig 
    module DivisionUpdate : 
      functor 
        (C : sig 
               module Dom : 
                 sig type kind = Sig.domain_is_field type v val z : v end 
               type coll 
             end) -> 
        sig val update : 'a -> 'a end 
    module Gen : 
      functor (C : Sig.COLL) -> 
        functor 
          (Update : functor 
                      (C : sig 
                             module Dom : 
                               sig 
                                 type kind = C.Dom.kind 
                                 type v 
                                 val z : v 
                               end 
                             type coll 
                           end) -> 
                      sig val update : C.Dom.v -> C.Dom.v end) -> 
          sig 
            module U : sig val update : C.Dom.v -> C.Dom.v end 
            val foo : C.Dom.v 
          end 
  end 
which seems fair enough.  When we start to "test" this, we get: 
module Test = GEF.Gen(Doms.GColl(Doms.FDomain))(GEF.DivisionUpdate);; 
let test = Test.foo;; 

#   module Test : 
  sig 
    module U : 
      sig 
        val update : 
          Doms.GColl(Doms.FDomain).Dom.v -> Doms.GColl(Doms.FDomain).Dom.v 
      end 
    val foo : Doms.GColl(Doms.FDomain).Dom.v 
  end 
# val test : Doms.GColl(Doms.FDomain).Dom.v = 0. 

Note how the type of update and foo look very "complex", even though the 
typechecker seems to know quite well that 'test' is actually of type 
float.  How is one supposed to know that the typechecker knows this and 
that ...Dom.v is not abstract? 

If we continue in that vein, contrast the following: 
module C_F = Doms.GColl(Doms.FDomain);; 
module Test1 = GEF.Gen(C_F)(GEF.DivisionUpdate);; (* works *) 

module C_I = Doms.GColl(Doms.IDomain);; 
module Test2 = GEF.Gen(C_I)(GEF.DivisionUpdate);; (* throws an error, as 
expected *) 

The biggest difference is that FDomain has kind = domain_is_field while 
IDomain has kind = domain_is_ring. 
Let's look at the printed type of C_F and Test1: 
#   module C_F : 
  sig 
    module Dom : 
      sig type kind = Doms.FDomain.kind type v = Doms.FDomain.v val z : 
v end 
    type coll = Dom.v list 
  end 
# module Test1 : 
  sig 
    module U : sig val update : C_F.Dom.v -> C_F.Dom.v end 
    val foo : C_F.Dom.v 
  end 

Why Doms.FDomain.kind instead of Sigs.domain_is_field for the kind?   
Since test1 *works*, clearly these are known to be the same. 
Also, not how foo has type C_F.Dom.v -- which one has to chase to Dom.v, 
to Doms.FDomain.v, and finally to float.  When this occurs in an error 
message, having to do 4 (or more) levels of type-expansions can be quite 
difficult.  (And misleading too, but that is a different issue). 

Now let's look at what we get for the rest: 
#   module C_I : 
  sig 
    module Dom : 
      sig type kind = Doms.IDomain.kind type v = Doms.IDomain.v val z : 
v end 
    type coll = Dom.v list 
  end 

and then a long error message for Test2, which ends with 
Modules do not match: 
  sig type kind = C_I.Dom.kind type v = Dom.v val z : v end 
is not included in 
  sig type kind = Sig.domain_is_field type v val z : v end 
Type declarations do not match: 
  type kind = C_I.Dom.kind 
is not included in 
  type kind = Sig.domain_is_field 

Now, C_I.Dom.kind is actually Sig.domain_is_ring -- why wasn't that 
printed?  That would have been SO much more informative!  In similar 
situations, one can take a long time chasing down why it seems that 
C_I.Dom.kind was somehow abstract when it should have been concrete, and 
so on. 

Would it be possible to get some switches to optionally ask for all 
types to be fully expanded?  Also, it would be nice to be able to 
visually distinguish between an abstract type and a concrete but elided 
type even when not asking for types to be expanded. 

Note that in other situations (the code is even larger), one can get a 
strange mixture of non-expanded, partially-expanded and fully-expanded 
types all for essentially the same situation, although it seems that 
this latter part may be due to MetaOCaml rather than OCaml.  But it is 
rather difficult to be certain... 

Jacques 

PS: the work that led up to this email is joint work with Oleg Kiselyov.
			

gettext for caml

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/a525ffca2dbf36e2/73d27f4cde549374#73d27f4cde549374

skaller asked and google talk answered:
> Has anyone done any stuff for localising Ocaml programs? 
> Something like GNU's gettext system? 


There is ocaml-gettext:  http://sylvain.le-gall.net/ocaml-gettext.html 
Only the version in svn seems to work with latest caml though, and i can't 
find a way to access svn exept through the web interface. Hehe.. 
But we are using it with some success in the demexp project: 
http://savannah.nongnu.org/projects/demexp
			
Sylvain Le Gall added:
Indeed, ocaml-gettext need to be re released soon. I am pretty busy with 
debian ocaml stuff right now, but i will rework on it ASAP.
			

Ocamlp3l

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/fdc2bbac7c8e31dc/5c38b94e526b7467#5c38b94e526b7467

skaller asked and Frédéric Gava answered:
> Does any one here know about Ocamlp3l: 
> http://www.pps.jussieu.fr/~dicosmo/ocamlp3l/ 

OCamlP3L is a library for OCaml for parallel skeleton programming (P3L 
skeletons). A parallel skeleton (also know as algorithm skeleton) is a 
"function" that could be implemented in parallel (the goal is to have a good 
set of such function : "easy" to be implemented and efficient and can 
express many parallel problems). 

For example, List.map. The list could be distributed on the processors and 
Map could be apply in parallel (if there are no side effects). 

You should read the papers of Roberto Di Cosmo (for example in the revue 
"parallel programming") about OCamlP3L and go to this web page (of Murray 
Cole, the "father" of parallel skeletons) about skeleton programming 
http://homepages.inf.ed.ac.uk/mic/Skeletons/index.html
			

Post-docs on formal compiler verification

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/4e0bc892ee745c8e/32150f598f850a95#32150f598f850a95

Xavier Leroy announced:
[ The following openings might interest members of this list, as it is 
  strongly concerned with (mechanized proofs of) pure functional 
  programs.  - Xavier Leroy ] 
The Compcert project, funded by the French National Agency for 
Research in its program on the security of computer systems 
(ANR-SSIA), is offering two post-doctoral positions for durations of 
up to 18 months, starting in the first half of 2007. 

The Compcert project is concerned with the formal description of 
optimizing compilers for high-level languages, including a significant 
subset of the C programming language, and computer-verified proofs of 
correctness for these compilers.  Foundational aspects of this project 
include the mechanization of programming language semantics and 
mechanically verified proofs of correctness for functional and 
imperative programs.  Most proofs and algorithms are verified using 
the Coq proof assistant. 

The project is looking for applicants having a solid background 
in one or preferably two of the following domains: 

  * programming language semantics, 
  * compiler development, 
  * computer-based proof assistants, 

and a real interest in the other aspects. 

The topics to be investigated during the post-docs range over the 
scope of the project, from formal compiler verification to mechanized 
semantics to connections with other tools (program provers, static 
analyzers) used to develop high-assurance software.  For instance, we 
envision the following two topics: 

 * A formalization of domain theory inside the type theory of the Coq 
   proof assistant and a study of its applications in the development 
   of correct functional programs, with a special focus on potentially 
   non-terminating programs such as interpreters, debuggers, or 
   semi-algorithms for optimisation problems. 

 * A study of separation logic for the Compcert subset of the C 
   programming language, including formal proofs of consistency 
   between this axiomatic semantics and the operational semantics used 
   in the compiler verification task. 

Proposals for other relevant topics are welcome and will be discussed 
between applicants and the investigators of the Compcert project: 
  Xavier Leroy (INRIA, main investigator), Yves Bertot (INRIA), 
  Sandrine Blazy (ENSIIE), Pierre Courtieu (CNAM), Damien Doligez (INRIA), 
   Pierre Letouzey (University of Paris 7), Laurence Rideau (INRIA). 

The positions are located either in Evry (Paris area, under the 
supervision of Sandrine Blazy) or Sophia Antipolis (Nice area, French 
Riviera, under the supervision of Yves Bertot). 

The gross salary is around 2200 Euros per month (1800 Euros net salary 
after deduction of social benefits). 

To apply, please send a detailed vitae and a research statement 
(indicating the topics on which you'd like to work) to the following 
address: compcert@yquem.inria.fr.  Other inquiries concerning these 
positions can be sent to this address as well.
			

Oracle OCCI C++ interface

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/0b4a5caed6cf71af/1d2244da3af86fa7#1d2244da3af86fa7

Serge Aleynikov announced:
I would like to announce availability of the OCaml client interface 
library for Oracle.  In the contrast to existing projects (oci8ml, 
eqoci) found elsewhere, this project uses Oracle 10g's OCCI C++ 
interface on top of OCI.  This allowed to implement a rich set of DML 
and DDL operations with the database.  The library requires installation 
of an Oracle 10g Instant Client library.  See doc/index.html file for 
installation instruction of prerequisites. 

The following operations with an Oracle database are supported: 

   - Simple DML operations including SELECT / INSERT / UPDATE / DELETE 
   - Parameterized DML operations including SELECT / INSERT / UPDATE / 
DELETE 
   - Execution of PL/SQL stored procedures 
   - Execution of bulk DML array INSERT / DELETE / UPDATE operations 
   - Oracle exception handling 
   - Oracle bulk exception handling with specifying failed rows and 
errors for each row 
   - Transaction control (commit and rollback) 
   - Automatic garbage control of Oracle resources (connections, statements 
     and cursors) 
   - Functional and Object-Oriented API included 

You'll need to modify the Makefile to include paths to an Oracle home 
and OCaml installation. 

The OCaml portion of the library is written in the revised syntax.  The 
following example illustrates one of the most powerful features of using 
array DML insert of records with exception-based control of failed rows 
(note that the entire array is sent to an Oracle database in a single 
network roundtrip): 

try 
     let n = statement#execute_array 
                 ~sql:"insert into test (id, name, dt, num) values (:1, 
:2, :3, :4)" 
                 [ 
                     [| Var_int 1; Var_str "AAA"; Null_date; Null_float |]; 
                     [| Var_int 2; Null_str;      Null_date; Null_float |]; 
                     [| Var_int 3; Null_str;      Null_date; Null_float |] 
                 ] 
     in 
         Printf.printf "Inserted %d records using array DML\n" n 
with [ORA_BULK_EXCEPTION (m, a) -> do { 
           print_endline m; 
           Array.iter (fun (i, e, m) -> Printf.printf "  Row[%d]: %d - 
%s\n" i e m) a 
       } 
]; 

The project home page is http://oracaml.sourceforge.net.  It contains 
links to documentation and download site. 

Your feedback and enhancement requests are welcome.
			

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