<thelema>
two versions (native/bytecode) of two compilers.
<orbitz>
mmm so much faster
<orbitz>
is there any interest at INRIA to give full stack traces on natively compiled applications?
<thelema>
already implemented.
<thelema>
(well, maybe not on all architectures, but x86 - yes)
<orbitz>
oh excellent
<orbitz>
in the current stable version?
<thelema>
compile with -g and use export OCAMLRUNPARAM="b1"
<thelema>
yes, in 3.10.2
<thelema>
I think in 3.10 even
<orbitz>
rockin!
<orbitz>
i've asked this before but quite honesty i forgot the answer. If I want a functional-style map object, is there any implementation that is polymorphic so I could, for instance, write a generic key_list function to give me a list of keys in the map?
<thelema>
the stdlib doesn't have that.
<thelema>
(that = polymorphic map)
<thelema>
you could pretty easily take the stdlib implementation and make one that uses Pervasives.(<) for compare
<thelema>
err, Pervasives.compare even
<thelema>
it shouldn't be difficult for your key_list function to take as parameters the/any needed function(s) from Map that it needs to use.
<thelema>
anyway, time to go. Good night all.
<orbitz>
night
thelema is now known as thelema|away
|Catch22| has quit ["To the best of my knowledge, I guess that I'm fresh"]
olleolleolle has joined #ocaml
olegfink has joined #ocaml
<olegfink>
hi
<orbitz>
hi
<olegfink>
while playing with ocaml's C interface accroding to the manual:
<olegfink>
$ ocamlc -custom -o test unix.cma test.ml lib.o
<olegfink>
lib.c:(.text+0x14): undefined reference to `CAMLparam2'
<olegfink>
etc.
<olegfink>
where are those things implemented and why doesn't ocaml pick them up automagically?
<Yoric[DT]>
I'm just wondering if it's close to something I already know: lambda-calculus, Abadi&Cardelli's Calculus of Objects, etc.
<thelema>
I'm suspicious about a claim in any useful system of proofs that are "not only possible but easy"...
<Yoric[DT]>
I need to give an appreciation to an application as lecturer, by someone who worked using Featherweight Java.
<Yoric[DT]>
Since I'm not really familiar with the calculus, I was wondering if anything could be summed up in less than 5 lines.
<thelema>
"There are three basic computation rules: one for field access, one for method invocation and one for casts" sounds like a ground-up design, specific to java.
<RobertFischer>
Uh, I'm assuming those aren't the only computation rules.
<RobertFischer>
I'd really like there to be some kind of branching structure.
* RobertFischer
hasn't checked out the webpage...just confused by the quote.
<thelema>
RobertFischer: does lambda calculus have a branching structure?
<RobertFischer>
I have no idea.
<RobertFischer>
Does it?
<RobertFischer>
Looks like it does.
<thelema>
It looks like lambda calculus does branching through piecewise function definition - like OCaml's function p1 -> e1 | p2 -> e2
<RobertFischer>
What's the "casts" thing all about, though? How does that map onto lambda calculus?
<RobertFischer>
Is that substitution?
<thelema>
but I think it's able to handle even boolean logic without piecewise functions.
<thelema>
no, I don't think their model maps to LC in a natural fashion.
<Yoric[DT]>
IIRC, un lambda-calculus, branching is done by defining booleans.
Linktim has quit [Read error: 110 (Connection timed out)]
<Yoric[DT]>
iirc, if you want to define branching piecewise, you need something like Amb
<Yoric[DT]>
which is not standard lambda-calculus
szell has joined #ocaml
jdev has quit [Read error: 104 (Connection reset by peer)]
jdev has joined #ocaml
schme has joined #ocaml
thelema is now known as thelema|away
Morphous_ has joined #ocaml
grom358 has quit ["Leaving"]
det has joined #ocaml
OChameau has joined #ocaml
det has quit [Client Quit]
det has joined #ocaml
Morphous has quit [Read error: 110 (Connection timed out)]
Linktim has joined #ocaml
evn has quit [Read error: 104 (Connection reset by peer)]
Axioplase has joined #ocaml
<mfp>
Yoric[DT]: TAPL says about Featherweight Java > "a contender for a minimal core calculus for modeling Java's type system. The design of FJ favors compactness over completeness almost obsessively, having just five forms of term: object creation, method invocation, field access, casting, and variables. Its syntax, typing rules, and operational semantics fit comfortably on a single (letter-sized) page. (...) FJ is only a little larger than the
<mfp>
lambda-calculus or Abadi and Cardelli's object calculus, and is significantly smaller than other formal models of class-based languages like Java (...) FJ's main application is modeling extensions of Java (...) because the proof of type safety for pure FJ is very simple, a rigorous safety proof for even a significant extension may remain manageable."
<Yoric[DT]>
thanks
<RobertFischer>
Interesting assertion re: the correlation between simplicity and manageability.
<RobertFischer>
(Not saying it's wrong. Just saying it's an interesting assertion.)
<Yoric[DT]>
It's often true.
<Yoric[DT]>
Not always, though.
<Yoric[DT]>
I'd say Mobile Ambients are simple but essentially unmanageable.
det has quit [Remote closed the connection]
pango_- has joined #ocaml
pango_ has quit [Remote closed the connection]
pango_- is now known as pango_
det has joined #ocaml
oc13 has quit [Read error: 110 (Connection timed out)]
|Catch22| has joined #ocaml
<RobertFischer>
Yoric[DT]: I'd say that list processing is pretty simple, but LISP gets unmanageable pretty fast. And RISC assembly programming has a similar problem. On the other hand, the complexity of Rails is one of the things that makes web-apps on Rails get unmanageable pretty fast.
<RobertFischer>
Hence, the interesting part of the interesting assertion.
schme has quit [Remote closed the connection]
bluestorm has joined #ocaml
schme has joined #ocaml
<Smerdyakov>
Simplicity of language definitions does tend to correlate with manageability of proofs about those languages.
<Yoric[DT]>
My remark was that Mobile Ambients are extremely simple but in this case, the simplicity of definition often gets in the way of provability.
<Smerdyakov>
Which theorems are hard to prove?
<Yoric[DT]>
It's not exactly that theorems are hard to prove. It's more that theorems are usually false, because the language is so very permissive, so finding out which subset of the language to use is hard.
<RobertFischer>
Smerdyakov: Good point. We're talking about "proofs about those languages", not the use of the language per se.
<RobertFischer>
Smerdyakov: I'd wandered off into a more general case.
Axioplase has quit ["bbl"]
pango_ has quit [Remote closed the connection]
<hcarty>
Any suggestions on where to look when a program leaks memory that is not freed after the program exits?
<hcarty>
The programs in question are written in OCaml, but use several C libaries. There is a memory leak somewhere, but to make matters worse the memory is not freed when the program exits.
<hcarty>
I have never had this problem before in any language, so I'm not sure where to start
<petchema>
you can use tools like valgrind to detect leaks on C side
<hcarty>
petchema: I'm trying that now. It's taking a while due to the large amount of stuff shuffling around in ram.
pango_ has joined #ocaml
<hcarty>
It also corrupts a ramdisk, which seems disturbing to me. But perhaps ramdisk ram isn't protected.
<petchema>
tmpfs ?
<hcarty>
/dev/ram allocated with ~550Mbytes and formatted to ext3
<petchema>
unless you access /dev/ram directory, it's allocated in kernel space so non-root processes shouldn't be able to corrupt it
<petchema>
s/directory/directly/
<petchema>
btw, why use a journaled fs with a ramdisk?
<hcarty>
Nope, all access is through the appropriate mount point.
<hcarty>
I'm not the admin on the system, but I would guess habit
<petchema>
that's silly
<hcarty>
At this point, I just want to know how it is being corrupted. It seems very strange.
<hcarty>
And the program which seems to do the corruption is running as a non-root user
ygr has quit [Remote closed the connection]
<hcarty>
It may be an journal-on-ramdisk issue though. I've requested that it be changed to ext2 as a test.
Morphous has joined #ocaml
RobertFischer has quit []
RobertFischer has joined #ocaml
RobertFischer has left #ocaml []
RobertFischer has joined #ocaml
<RobertFischer>
mn
Morphous_ has quit [Read error: 110 (Connection timed out)]
Demitar has quit [Read error: 110 (Connection timed out)]
<olegfink>
any pointer to a C binding /without/ ocamlmklib?
<Yoric[DT]>
hi
<olegfink>
I need an example (turned out I'm too dump to figure out what to do myself from the manual) of making a binding to C
* Yoric[DT]
never tried, I'm afraid.
<olegfink>
err, s/dump/dumb/
<olegfink>
I've tried to literally follow the manual, and seems ocamlc doesn't provide something with CAMLreturn/CAMLparam/etc. stuff, so the C linker is unhappy
<det>
You mean, how to compile it?
<olegfink>
yep
<olegfink>
or any working example
<olegfink>
ocamlmklib is nice, but lacks mingw support