Hello
Here is the latest Caml Weekly News, for the week of October 24 to November 07, 2006.
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.
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...
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
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/
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.
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.
> 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/demexpSylvain 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.
> 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
[ 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.
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.
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.
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.