Here is the latest Caml Weekly News, for the week of 09 to 16 August, 2005.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30103John 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)
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30116Richard Jones announced:
A very tiny library implementing the "Double Metaphone" algorithm: http://merjis.com/developers/metaphone
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30121David 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
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30105Romildo 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.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30123Richard 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/
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/30134Yaron 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: email@example.com
Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).
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.