Hello
Here is the latest Caml Weekly News, for the week of May 16 to 23, 2006.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/32963/focus=32963
Christian Lindig announced:
To lookup types of identifiers from within Vim, I have implemented a
small tool in Ocaml called annot:
$ annot -type 30 20 main.annot
string list
Given a cursor position (line 30, column 20) it looks up the type
annotation for that position in main.annot. It is trivial to hook this
to a key in Vim, and probably most other editors.
function! OCamlType()
let col = col('.')
let line = line('.')
let file = expand("%:p:r")
echo system("annot -n -type " . line . " " . col . " " . file .
".annot")
endfunction
map ,t :call OCamlType()<return>
I'm well aware that Vim and Emacs have their own solutions, using their
own scripting languages, but I think it is better to have one general
solution.
You can download the tool from my subversion repository; it is released
under a BSD-style license.
svn co svn://svn.vistabella.de/annot
The tool should build on Unix systems, comes with ./configure, and a
manual page. Let me know if there are any problems. Of course, positive
feedback is also welcome.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/32945/focus=32959
Continuing the thread from last week, Alain Frisch said:
Nicolas Pouillard wrote:
> The last four months, I have been working on the Camlp4 renovation
> with Michel Mauny.
>
> We are glad to announce the beta-release of a new version of Camlp4,
> that contains a lot of major changes.
>
> *** This version is not backward compatible. Use it at your own risk.***
>
> Major changes are described at:
> http://gallium.inria.fr/~pouillar/camlp4-changes.html
Wow, that's a major renovation indeed. Great news, good job.
I've been able to upgrade two of my syntax extensions [1][2] without any
problem and the code is now cleaner than before. Some people might want
to look at them for examples of simple syntax extensions working with
the new Camlp4.
Thanks Nicolas!
-- Alain
[1] openin: http://www.eleves.ens.fr/home/frisch/soft.html#openin
[2] ulex: http://www.cduce.org/download.html#side
Stefano Zacchiroli asked and Nicolas Pouillard answered:
> What are the plans for the future of camlp4, and especially for the
> changes you made? Are them going to be integrated in the "official"
> camlp4 release and thus integrated in future releases of ocaml? Will
> camlp4 be distributed separately in the future?
It's planned to be integrated in the future releases of OCaml.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/32965/focus=32965
Dan Koppel asked:
I would like to report what I think might be a bug in the Ocaml compiler. But
first I wanted to run this by this group in case there's something I'm missing.
I have some very simple code that consists of 2 nested loops. Inside the inner
loop, is a simple statement. Furthermore, the inner loop is not "tight". Ie.
the number of iterations within the inner loop is very large and the number of
iterations of the outer loop is very small. I then manually time this. I then
change the code by inserting a simple function call between the inner and outer
loops. This should have virtually no effect whatsoever. However, when I time
this, I get exactly twice the time. This is somewhat inexplicable. I tried
tinkering with the "-inline" option for ocamlopt but this had no effect. Below
is the actual code (main.ml):
let main () =
let dummy1 = ref 0 in
let dummy2 = ref 0.0 in
for i = 1 to 4 do
for j = 1 to 1000000000 do
dummy1 := !dummy1 + 1;
dummy1 := !dummy1 - 1
done;
dummy2 := Unix.gettimeofday ()
done
let _ = main ()
I compile as follows: ocamlopt unix.cmxa main.ml
and run: ./a.out
Is this in fact a bug of the ocamlopt compiler? Or is there some way currently
to make this effect disappear?
John Carr answered:
On SPARC the presence of the function call in the outer loop causes
the code generated for the inner loop to change so the dummy1 variable
is stored on the stack instead of in a register. Each loop iteration
loads dummy1, modifies it, and stores it back onto the stack.
The store-load hazard, loading a value that is in the store buffer,
adds a large delay. The loop runs in half the time if I comment out
either the store or the load in the assembly.
If the inner loop did more computation the effect would be much less.
This is surprising but not strictly a bug. Xavier Leroy has posted
about similar minor changes causing the compiler to box or unbox a
floating point value with major changes in performance.
Xavier Leroy also answered:
As John Carr mentioned, the function call forces the variables that
are live across the call (i.e. dummy1) to be spilled, causing one additional
memory read and one additional write at each iteration of the inner
loop. Since your inner loop is approximately 4 integer instructions,
the additional memory traffic can easily halve performance.
I grant you that spill code generation could be more clever here and
spill/reload around the whole inner loop. But, no, it's not a bug:
Ocaml has a bug when the generated code crashes or produces incorrect
results.
> I learned in basic compiler theory that when a function is called, you
> save all the registers before entering the function.
That's an over-simplification. First, many compilers designate a
number of registers as "callee-save", meaning that all functions must
preserve their values. These would be preserved across a call.
It happens that ocamlopt does not implement callee-save registers, as
they make garbage collection (more exactly, stack traversal) and
exception handling more expensive. But even when a function call
destroys all registers, as with ocamlopt, there are many possible
placements for spills (saving a register in the stack) and reloads (of
a register from the stack), and the placement you suggest (only around
calls) is rarely optimal. Well, in your example it is :)
Generation of spill code is a dark corner of compiler construction.
As with many other compilation problems, there are a bunch of
NP-completeness results. Unlike many other compilation problems, I'm
not aware of any published heuristics that works well in most cases.
Well, there is the paper by George and Appel where they use an ILP
solver (integer linear programming) to produce optimal spills, but
that's kind of expensive...
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/32949/focus=32949
Continuing the thread from last week, Frederick Akalin asked and Brian Hurt answered:
> I'm running into cases where the 4 MB limit on arrays is starting to become a
> problem. Lists are much slower and cause seg faults for me on the same data
> set, and Bigarrays are a partial solution because I'd like to be able to
> store arbitrary types in arrays (not just numbers).
>
> I was greatly surprised when I found out there was such a low limit on
> arrays. Is there a reason for this? Will this limit ever be increased?
It comes from how arrays are stored in memory. Every boxed value has a
"tag word", which, among other uses, is used by the GC to figure out how
big the object is (i.e. where the next object starts). Now, the encoding
scheme of this tag word is fairly complicated, but it works out that for
arrays, 10 bits of the 32 bits is used for other stuff, leaving 22 bits
for the size. This limits the size of an array to 4M-1 elements
(actually, it limits the size of the array to 16M-4 bytes, as size is
measured in words- which is why arrays of floats are limited to 2M-1
entries- each float takes up 8 bytes aka 2 words).
When you move to 64 bits, the tag word doubles in size, but the amount of
"other" information in the tag word doesn't- this means that suddenly you
have 52 bits of size, or 4T arrays. And now floats only take up one word,
not two, so they too can have 4T arrays.
The array of array idea someone brought up is a good one. There's a
slight performance hit, but not much. I'd keep the top level array short-
1K entries is enough. The advantage of this is that if you're heavily
using the array, the top level array will stay in cache (possibly even L1
cache), meaning the main cost of an array access only goes up by about 10%
or so, maybe less (maybe 1% if it stays in L1 cache). The reasoning goes
like this: the largest cost by far of an array access on a large array is
the cache miss. Doing a memory reference that is satisified out of L1
cache generally takes 1-4 clock cycles. If you have to go to L2 cache,
that's going to take 10-40 clock cycles (approximately). Going to main
memory? 100-350+ clock cycles. With a large array, you're likely going
to take the 100-350+ clock cycle hit anyways. If the top level array is in
L1 cache, you're only adding 1-4 clockcycles to the 100-350+ clock cycle
hit you're going to take anyways.
Personally, I think PCs should have gone 64 bit circa 1997 or so. Once we
started getting hard disks large enough that we couldn't mmap the entire
hard disk, we started hitting problems. Long long and the large file
interfaces are examples of these problems. The longer we go- and the
larger memories and hard disks get, the bigger the problems get.
Microsoft seems to be the main impediment, now that AMD has forced Intel
to get off the stick.
> If I had a record type with 5 floats,
> will the limit then by Sys.max_array_size / 10?
Within the record, the floats are unboxed (assuming you didn't have any
non-float elements). This means the floats are stored directly in the
record, and that the record doesn't hold pointers to the floats. But the
record itself is boxed- which means that an array of these records is
really an array of pointers to these records, meaning that you're back at
the 4M-1 limit.
Note that a record of 5 floats costs 44 bytes (40 bytes for the 5 floats +
4 bytes for the tag word). Assuming no records are stored in more than
one location, the total memory cost of an array of 4M-1 of them is 16M for
the array, plus (4M-1)*44 for the records, for a total of 192M-44 bytes.
This is almost 10% of your available memory space right there.
> Is there some sort of
> existing ArrayList module that works around this problem? Ideally, I'd like
> to have something like C++'s std::vector<> type, which can be dynamically
> resized.
Ocaml can't dynamically resize arrays. This gets tricky to do when arrays
get large. At the extreme, if the array takes up 50% + 1 byte of the
total address space, you can't resize it to be any larger- to resize
requires you to copy it, which takes more memory than you have. I've
seend problems well before then.
> Also, the fact that using lists crashes for the same data set is surprising.
> Is there a similar hard limit for lists, or would this be a bug? Should I
> post a test case?
I'm willing to bet dollars to donuts that the problem you hit with lists
was stack overflow. Without signifigantly impacting performance there
isn't a whole lot Ocaml can do about detecting stack overflow before the
segfault hits. My general rule is, if it's going to contain more than a
few dozen items, it probably shouldn't be a list. Extlib's library is
less prone to this error, but you can still run into serious problems with
long lists.
Xavier Leroy also answered:
> I was greatly surprised when I found out there was such a low limit on
> arrays. Is there a reason for this? Will this limit ever be increased?
As Brian Hurt explained, this limit comes from the fact that heap
object sizes are stored in N-10 bits, where N is the bit width of the
processor (32 or 64).
Historical digression: this representation decision was initially
taken when designing Caml Light in 1989-1990. At that time, even
professional workstations had 16 M of RAM at best, so limiting arrays to
4M elements was reasonable. The decision was then reconsidered in
1995 during the redesign that led to OCaml. At that time,
64-bit architectures were all the rage: OCaml was actually implemented
on a 64-bit Alpha, and only then backported to 32-bit machines.
So, the original header format was kept, since it makes complete sense
on a 64-bit architecture. Little did I know that the 32-bitters would
survive so long. Now, it's 2006, and 64-bit processors are becoming
universally available, in desktop machines at least. (I've been
running an AMD64 PC at home since january 2005 with absolutely zero
problems.) So, no the data representations of OCaml are not going to
change to lift the array size limit on 32-bit machines.
> Is the limit a limit on the number of elements or the total size? The
> language in Sys.max_array_size implies the former, but the fact the
> limit is halved for floats implies the latter. If I had a record type
> with 5 floats, will the limit then by Sys.max_array_size / 10?
No. In general, Caml arrays are not unboxed, meaning that your array
of 5-float records is actually an array of pointers to individual
blocks holding 5 floats. The only exception is for arrays of floats,
which are unboxed.
> Is there
> some sort of existing ArrayList module that works around this problem?
> Ideally, I'd like to have something like C++'s std::vector<> type, which
> can be dynamically resized. Do I have to write my own? :(
A better idea would be to determine exactly what data structure you need:
which abstract operations, what performance requirements, etc. C++
and Lisp programmers tend to encode everything as arrays or lists,
respectively, but quite often these are not the best data structure
for the application of interest.
> Also, the fact that using lists crashes for the same data set is
> surprising. Is there a similar hard limit for lists, or would this be a
> bug? Should I post a test case?
Depends on the platform you use. In principle, Caml should report
stack overflows cleanly, by throwing a Stack_overflow exception.
However, this is hard to do in native code as it depends a lot on the
processor and OS used. So, some combinations (e.g. x86/Linux) will
report stack overflows via an exception, and others will let the
kernel generate a segfault.
If you're getting the segfault under x86/Linux for instance, please
post a test case on the bug tracking system. It's high time that
Damien shaves
Nicolas Cannasse said and Xavier Leroy answered:
> A segfault will happen on Windows/MSVC port. I also found some cases
> where the commandline program (the haXe compiler in that case) just
> silently exited on Stack Overflow (exit code was not 0 but no error or
> "program error" infamous message box was displayed).
>
> I think that there is some MSVC specific C extension for catching such
> stack overflows (__try / __except*). It would be nice to have such a
> handling at the ocaml toplevel that would at least exit with a
> meaningful error message. I don't care so much in my case since I'm not
> using C code a lot, I know for sure that any crash/early abort is
> indeeed a stack overflow. That might not be the case for all Win32 users.
>
> Best,
>
> Nicolas
> *
> http://msdn.microsoft.com/library/default.asp?url=/library/en-us/vccelng/htm/key_s-z_4.asp
I'm aware of __try/__finally, but a bit of experimentation suggested
that it doesn't play nice with OCaml's exception handling. There is a
lower-level API whose name I cannot remember that might be usable
within Caml, but I didn't pursue this. Windows users are welcome to
contribute suggestions or code.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/33015/focus=33015
John Harrison announced:
I'm pleased to announce the release of version 2.20 of the HOL
Light theorem prover, available now from the HOL Light homepage:
http://www.cl.cam.ac.uk/users/jrh13/hol-light/index.html
Since the last release, the system has been cleaned up, with many
"internal" functions deleted or hidden. There is now a reference
manual, available as crosslinked HTML or as a single PDF file, that
documents all the inference rules, conversions, tactics and utility
functions defined in the system:
http://www.cl.cam.ac.uk/users/jrh13/hol-light/reference.html
Besides this consolidation and documentation, there are several new
features, improvements and bugfixes. Those I consider most important
are listed below.
John.
MOST SIGNIFICANT CHANGES
------------------------
* Better infrastructure for the integers including automation
of divisibility properties (more details below).
* Much improved performance of ARITH_RULE on problems with many
instances of cutoff subtraction.
* Much improved performance of the ring and field functions on
large problems.
* Generalized beta conversion (e.g. (\(x,y). x + y) (1,2) = 1 + 2)
is now built into the default "rewrites"
* Online help is available (do ``help "ident";;'')
* Type abbreviations are supported (see "new_type_abbrev")
* Binary numerals are also accepted ("0b101010")
* "define_finite_type", for defining indexing types, has been
added.
MOST ANNOYING INCOMPATIBLE CHANGES
----------------------------------
Two constant name changes:
dest_int -> real_of_int
mk_int -> int_of_real
the renaming of these utility functions:
is_beq -> is_iff
[dest|is|mk]_intconst -> [dest|is|mk]_realintconst
upto -> --
gather -> filter
and the following theorem renamings (some others about iterated
operations had a few redundant hypotheses removed)
[N]SUM_CMUL -> [N]SUM_LMUL (and there's an _RMUL version too)
NEW INTEGER SUPPORT
-------------------
The type `:int` was formerly a poor relation of `:num` and `:real`, with
rather less in the way of syntax operations and automated support. This
has mostly changed. There are now syntax operations like "mk_intconst",
arithmetic conversions like "INT_ADD_CONV" and "INT_REDUCE_CONV" and an
instantiation of the ring procedure, "INT_RING".
The most basic divisibility notions "divides", "coprime" and "gcd" have
been defined on both integers and natural numbers in the core. Few
lemmas about them have been provided, but there are some very useful
(though hacky and brittle) automated proof procedures that can
generate many routine lemmas about divisibility notions automatically:
NUMBER_RULE and NUMBER_TAC (over the natural numbers) and INTEGER_RULE
and INTEGER_TAC (over the integers). For example, over the natural
numbers:
NUMBER_RULE `coprime(x * y,x EXP 2 + y EXP 2) <=> coprime(x,y)`;;
NUMBER_RULE `!d a b:num. d divides (a * b) /\ coprime(d,a) ==> d divides b`;;
NUMBER_RULE `~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
==> coprime(a',b')`
NUMBER_RULE `!a x y:num.
coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`;;
Over the integers, even some existential goals can be solved, e.g. the
2-variable Chinese remainder theorem. This works less well over the
natural numbers because of the positivity constraints, though I plan to
fix this eventually:
INTEGER_RULE
`!a b u v:int. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`;;
INTEGER_RULE
`gcd(a,n) divides b ==> ?x:int. (a * x == b) (mod n)`;;
NEW EXAMPLES/LIBRARIES
----------------------
Examples/binary.ml --- binary expansion of numbers
Examples/combin.ml --- combinatory logic (port of old HOL88 example)
Examples/ste.ml --- basic Symbolic Trajectory Evaluation theory
Multivariate/clifford.ml --- multivectors with outer and geometric product
100/*.ml --- Some of the "great 100 theorems"
The last bunch of examples are HOL Light formalizations of some of the
theorems from the following list:
http://www.cs.ru.nl/~freek/100/
I believe that all the ones done in HOL Light are either in this
directory or somewhere in the standard core or libraries.
Archive: http://thread.gmane.org/gmane.comp.lang.caml.general/33031/focus=33031
Frederick Akalin asked and Jacques Garrigue answered:
> At the risk of starting another flamewar, I have another question. I
> notice that if I have a record type that's defined in an .mli file, I
> am able to print objects of that type and see its contents in the
> debugger. However, if I make that type abstract (only defining it in
> the .ml file), I am unable to do so, instead seeing "<abstr>", unless
> I am in the .ml file where the type is defined.
>
> Surely this information is available to the debugger from anywhere in
> the program? Currently I make most of my types non-abstract simply
> because it is impossible to debug my programs without being able to
> check record contents, a practice which I would like to avoid having
> to do. I am used to gdb, which prints out all a struct's contents
> regardless of protected/private modifiers, or Perl, which provides a
> similar facility with the Data::Dumper module.
To be more precise, the debugger uses information from the .cmi file
to print values. The information is not included in the .cmo file,
even with the -g option. Printing automatically abstract type would
require a new infrastructure, saving type definitions in the .cmo.
Note that an intermediate step would be to declare your definitions as
private: they become semi-abstract (you cannot create values from
outside the module), but you can still print them.
> I am aware that the debugger lets you load printing functions, a
> facility which I am now exploring. Although my first impression is
> that it requires a non-trivial amount of work, both on the coding and
> debugging side.
This requires some work, but not as difficult as it may seem.
The pretty-printer is very easy to use, particularly Format.fprintf.
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.