[cwn] Attn: Development Editor, Latest Caml Weekly News
Alan Schmitt
alan.schmitt at polytechnique.org
Tue Nov 7 00:55:09 PST 2006
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
========================================================================
1) 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.
========================================================================
2) 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...
========================================================================
3) 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>
========================================================================
4) 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/>
========================================================================
5) 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.
========================================================================
6) 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.
========================================================================
7) 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.
========================================================================
8) 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>
========================================================================
9) 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 at yquem.inria.fr. Other inquiries concerning these
positions can be sent to this address as well.
========================================================================
10) 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
(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/20061107/b45a16a0/attachment.pgp
More information about the caml-news-weekly
mailing list