[cwn] Attn: Development Editor, Latest Caml Weekly News
Alan Schmitt
alan.schmitt at polytechnique.org
Tue Aug 16 02:08:17 PDT 2005
Hello,
Here is the latest Caml Weekly News, for the week of 09 to 16 August,
2005.
1) New OCaml version of HOL Light theorem prover
2) Library implementing double metaphone phonetic algorithm
3) demexp 0.6
4) Plot library
5) Adwords API
6) Job Posting
========================================================================
1) New OCaml version of HOL Light theorem prover
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30103>
------------------------------------------------------------------------
** John Harrison announced:
I'm pleased to announce the availability of the HOL Light theorem prover
version 2.0, based on Objective Caml. The system and its documentation,
including a new draft tutorial, can be downloaded from the following Web
page:
<http://www.cl.cam.ac.uk/users/jrh/hol-light>
HOL Light proves theorems in classical higher-order logic. It is
intended
as an interactive proof assistant, but offers automated support for
proofs in some domains (arithmetic, algebra, pure logic...) and has a
significant library of pre-proved mathematics, particularly elementary
analysis. The system is designed to be fully programmable; not only is
OCaml the implementation language but the OCaml toplevel is the "shell"
from which the user directs proofs. Here are the proofs of a few
extremely simple theorems in the system, just to show you what it looks
like.
1. The sum of squares of the first n natural numbers, by induction and
arithmetic:
let SUM_OF_SQUARES = prove
(`!n:num. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1))
DIV 6`,
INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
ARITH_TAC);;
2. Vector version of Pythagoras's theorem, using algebra on vectors
and real
numbers:
needs "Multivariate/vectors.ml";;
let PYTHAGORAS = prove
(`!A B C:real^2.
orthogonal (A - B) (C - B)
==> dist(A,C) pow 2 = dist(B,A) pow 2 + dist(B,C) pow 2`,
SIMP_TAC[dist; NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB;
DOT_SYM] THEN
CONV_TAC REAL_RING);;
3. Los's "non-obvious" theorem of predicate calculus, using pure
first-order reasoning.
let LOS = prove
(`(!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)`,
MESON_TAC[]);;
The ASCIIfied logical symbols used above include:
!x. for all x
/\ and
\/ or
==> implies
\x. lambda x (like "fun x ->" in OCaml)
========================================================================
2) Library implementing double metaphone phonetic algorithm
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30116>
------------------------------------------------------------------------
** Richard Jones announced:
A very tiny library implementing the "Double Metaphone" algorithm:
<http://merjis.com/developers/metaphone>
========================================================================
3) demexp 0.6
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30121>
------------------------------------------------------------------------
** David Mentre announced:
I'm please to announce the availability of demexp 0.6, which is
programmed in OCaml.
Short announcement
------------------
demexp 0.6 is out! demexp is an electronic voting system for wide scale
direct democracy. demexp is a software developped for the democratic
experience project (<http://www.demexp.org>), but it can be used in
other
contexts (communities, firms, ...).
Compared to previous stable version 0.4, version 0.6 mainly focuses on
making the client more user friendly: support of demexp:// URL, support
of multiple servers at once, change tracking on the server, caching.
Longer announcement
-------------------
* What is demexp?
demexp is an electronic voting system for wide scale direct democracy.
demexp is developed mainly to support the democractic experience
project (<http://www.demexp.org>), but can be used in other contexts
(communities, firms, ...).
Briefly, demexp allows:
- to ask questions;
- to propose reponses to those questions;
- to vote on proposed responses (using Condorcet voting system).
demexp is implemented as a centralized server and a GTK2 graphical
client. A classification system allows to navigate through questions.
Dialog between client and server in implemented using IETF ONC RPC. The
server saves its bases in XML format.
* Where can I see screenshots?
You can see them at:
<http://www.nongnu.org/demexp/#screenshots>
* What's new in 0.6?
Release 0.6 features mainly client improvements compared to latest
stable 0.4.
o On client:
- display meaningful error messages in case of connection error;
- display number of votes on a question;
- no longer display of question's and responses' authors;
- client information are saved in a .demexp/ directory;
- client icon (Thomas Petazzoni);
- man page for client (Thomas Petazzoni, me);
- handling of multiple servers at once;
- support of demexp:// URL:
- to browse: demexp://server[:port]
- to see a specific question:
demexp://server[:port]/browse/question/78
- to vote on a specific question:
demexp://server[:port]/vote/question/78
- improvement of tag and question display in browser;
- network request caching (improves response time);
- new flags New/Voted/Updated in browser:
- New: the question has never been seen or has been updated on
the server;
- Voted: the user has voted on the question;
- Updated: the user has voted on the question and it has been
updated on the server.
- tag and question columns can be sorted;
- documentation of demexp URL handling in Gnome (Thomas de
Grenier de
Latour).
o On server:
- new RPCs to support above client improvements;
- redesign of RSS stream, for easier question access and processing
by external software;
- man page for server (Thomas Petazzoni, me);
- update to latest CDuce 0.3 release (Thomas Petazzoni);
- new RPC server_timers() to get information about server behaviour;
- handling of signals sent to server, graceful shutdown;
- automatic addition of a tag specific to each question;
- saving of server PID in a file;
- new --logfile and --daemon options on server.
o For both:
- code refactoring, the literate form of client and server is now in
a single document;
- ./configure script with improved detection of environment.
And of course, various bug fixes! :)
* How can I try it?
Get a binary client at:
<http://www.linux-france.org/~dmentre/demexp/binaries/>
Then use it to connect to the demonstration server:
$ demexp-gtk-client-0.6-x86 demexp://tuxinette.linux-france.org:50000
You can create your own login if you want. Use the "root" account
(password "demexp") to connect to the above server a create a new
account. Then change your Preferences and reconnect to the server by
relaunching the client.
Packages are also alvailable for various Linux distributions. Have a
loot at:
<http://www.nongnu.org/demexp/#packages>
* Where is the source code? In which language? Under which license?
The source code is available at:
<http://www.linux-france.org/~dmentre/demexp/latest-src/>
demexp is developed in Objective Caml (aka OCaml) language:
<http://caml.inria.fr/>
The code is developped in a literate programming form. You can see its
result at:
<http://www.linux-france.org/~dmentre/demexp/latest-src/demexp-
book-0.6.pdf>
Main code is under GNU General Public License (GPL). It relies on
external libraries and code of which licenses are GPL compatible (see
source code for details).
* Why should I contribute?
Because the project is fun, encompassing all Computer Science, from
network to cryptography though graphical user interfaces, databases,
etc.
Because the political project is interesting.
Because you have nothing better to do and you want to do some OCaml
hacking. ;)
* Links ?
Development: <http://savannah.nongnu.org/projects/demexp>
demexp software web site: <http://www.nongnu.org/demexp/>
Democratic experience political project: <http://www.demexp.org>
Web site and ideas to improve client design:
<http://www.demexp.org/dokuwiki/doku.php?
id=client:client_ergonomics>
========================================================================
4) Plot library
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30105>
------------------------------------------------------------------------
** Romildo asked and Chris King answered:
> I am looking for an ocaml plot library that integrates
> well with lablgtk. Is there one?
I've used the Gnome Canvas widget in lablgtk2 with much success. It's
included with lablgtk2 in "lablgnomecanvas.cma". It's based on Tk's
canvas widget but is much more powerful. Unfortunately it's not
available for lablgtk, only lablgtk2. You can find docs for it at
<http://compiler.kaist.ac.kr/~shoh/ocaml/lablgtk2/lablgtk-2.4.0/doc/
html/GnoCanvas.html> .
** Romildo and Ken Rose asked, and Chris King answered:
Romildo wrote:
> Does it work in Windows too?
It doesn't seem to be included in the Win32 distribution of LablGTK2,
but if you're using Cygwin then I presume it will compile given the
right libraries.
Ken Rose wrote:
>
> And can you print it?
No. This is one area in which the Gnome Canvas is actually inferior
to the Tk canvas widget.
========================================================================
5) Adwords API
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30123>
------------------------------------------------------------------------
** Richard Jones announced:
I guess this probably won't be of much interest to people on this
list, but for the record we released our Adwords API today under the
LGPL and GPL. It uses OC-SOAP and has various command line tools and
interactive interfaces to Adwords.
For more information:
<http://merjis.com/developers/adwords_api>
<http://merjis.com/developers/adwords_api#Features>
<http://groups.google.co.uk/group/adwords-api/browse_thread/thread/
1dc2c1c480504e52/e63adc2c387bb66e?hl=en#e63adc2c387bb66e>
<http://www.google.com/apis/adwords/>
========================================================================
6) Job Posting
Archive: <http://thread.gmane.org/gmane.comp.lang.caml.general/30134>
------------------------------------------------------------------------
** Yaron Minsky announced:
Jane Street Capital (<http://janestcapital.com>) is a proprietary
trading company located in Manhattan. We're looking to hire people to
work both as quantitative researchers and as systems-oriented
developers, as well as people who would like to combine both roles.
We're also looking for students interested in internships for next
summer (though it's perhaps a bit early to worry about that...)
Jane Street is an open and informal environment (you can wear shorts
and a t-shirt to the office), and the work is technically challenging,
including systems programming, machine learning, statistical analysis,
parallel processing, and anything that crosses our path that looks
useful.
One unusual attraction of the job is that the large majority of our
programming is done in OCaml. Pay is competitive, and we're a
reasonably small company (around 90 employees), so advancement is
pretty quick for someone who performs well.
Here's what we're looking for:
- A commitment to the practical. Both development and research are
tightly integrated with our trading operation, and we work very
hard to keep our work relevant. One of the big attractions of the
job is the opportunity to apply serious ideas to real-world
problems.
- Great communication skills. We need people who can explain
things clearly and cogently, who can read dense academic papers
and write clear documentation.
- Strong programming skills. Pretty much all of our programming is
in OCaml, so being a solid Caml hacker is a big plus. Extra points
for deep knowledge of OCaml internals and experience wrapping
thorny libraries. But we're also interested in great programmers
who we are convinced will be able to pick up OCaml quickly, so
anyone with high-level of proficiency with functional languages
would be a good match.
- Top-notch mathematical and analytic skills. We want people who
can solve difficult technical problems, and think clearly and
mathematically about all sorts of problems.
- Strong Unix/Linux skills --- We're looking for someone who knows
their way around the standard Unix tools, can write makefiles,
shell scripts, etc. We're also very interested in people with
serious systems administration and architecture experience.
If you're interested (or have any students you think might be a good
match) and would be willing to relocate to New York, please send a
cover-letter and resume to:
yminsky at janestcapital.com
========================================================================
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://sardes.inrialpes.fr/~aschmitt/cwn/>) or the RSS
feed of the
archives (<http://sardes.inrialpes.fr/~aschmitt/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://sardes.inrialpes.fr/~aschmitt/>
--
The hacker: someone who figured this 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/20050816/1fdcddaf/PGP.bin
More information about the caml-news-weekly
mailing list