|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
love-pingoo has quit ["Connection reset by pear"]
authentic has quit [Connection timed out]
^authentic is now known as authentic
pierre- has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
altmattr has joined #ocaml
comglz has quit ["Lost terminal"]
altmattr has quit []
altmattr has joined #ocaml
Axioplase_ is now known as Axioplase
<altmattr>
is it possible to get ocaml to generate so files?
<mrvn>
cmxo/cmxa files
<altmattr>
what exactly are those?
<mrvn>
.o/.a files.
<altmattr>
ah, so why do they have those extensions?
<mrvn>
Because they are a bit more than just binary blobs. For example ocaml can do inlining accross compilation units.
<altmattr>
nice, so there is extra info in there for ocamlopt but it can still be used just as a normal .o/.a file?
<mrvn>
no, just by ocaml.
<altmattr>
right
<altmattr>
so I need libs that I can use from other languages
<altmattr>
or just c realy
<altmattr>
really
<mrvn>
You can probably build a .so file with proper C bindings for the ocaml functions but don't ask me what would happen if you have 2 such libs.
<altmattr>
I am sure one will do :)
<altmattr>
how would I go about this?
<mrvn>
Then read up about how to use ocaml with main() being a C function.
<altmattr>
ah - it looks like -output-obj for ocamlopt is what I want
<altmattr>
thanks
<mrvn>
altmattr: you need caml_enter_blocking_section() and caml_leave_blocking_section() if you want to support multithreading.
<altmattr>
eek
<altmattr>
sounds scary
<mrvn>
ocaml doesn't allow actualy 2 threads running in parallel. But you can run stuff that doesn't use ocaml in parallel with an ocaml using thread. The two functions just tell when you start/end using ocaml for the time being.
<altmattr>
right
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
schme has joined #ocaml
middayc__ has joined #ocaml
middayc has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Operation timed out]
|jedai| has joined #ocaml
Demitar has joined #ocaml
seafood has quit []
_jedai_ has joined #ocaml
|jedai| has quit [Connection timed out]
altmattr has quit []
schme has quit ["leaving"]
altmattr has joined #ocaml
_jedai_ has quit [Operation timed out]
jeremiah has quit [Read error: 104 (Connection reset by peer)]
|jedai| has joined #ocaml
altmattr has quit []
altmattr has joined #ocaml
jeremiah has joined #ocaml
middayc__ has quit ["Ex-Chat"]
altmattr has quit []
altmattr has joined #ocaml
Yoric[DT] has joined #ocaml
altmattr has quit []
<Yoric[DT]>
hi
<thelema>
hi Yoric[DT]
<Yoric[DT]>
How do you do?
<thelema>
I'm all right. Keeping all too busy, it seems.
<thelema>
you?
<tsuyoshi>
wow osx sucks
<tsuyoshi>
I've spent two days just trying to get ocaml to compile
<mrvn>
I just apt-get installed it. :)
<tsuyoshi>
osx has apt-get?
^authentic has joined #ocaml
<tsuyoshi>
oh it doesn't matter, I don't have root
<thelema>
tsuyoshi: no apt-get for osx, only linux.
<thelema>
tsuyoshi: what do you get when you download tarball and do [./configure && make world]?
authentic has quit [Read error: 104 (Connection reset by peer)]
^authentic is now known as authentic
<tsuyoshi>
thelema: I forget.. there was a bug in ld
<tsuyoshi>
so I started trying to compile binutils
<tsuyoshi>
and that didn't work either
<thelema>
tsuyoshi: that's going to be tough. I remember ocaml having worked around a bug in ld recently. what version of osx?
<tsuyoshi>
that's today
<tsuyoshi>
yesterday I spent dealing with buggy nfs
<thelema>
good luck on that.
<tsuyoshi>
I need to see if we can install linux on this sucker..
realtime has joined #ocaml
<tsuyoshi>
nope
<Yoric[DT]>
thelema: technically, there's an apt-get for Linux.
<Yoric[DT]>
(part of Fink, iirc)
<Yoric[DT]>
Time to go teach, though.
<Yoric[DT]>
Cheers.
Yoric[DT] has quit ["Ex-Chat"]
seafood has joined #ocaml
<tsuyoshi>
oh I see.. gnu binutils doesn't work on osx at all
seafood has quit [Client Quit]
altmattr has joined #ocaml
_jedai_ has joined #ocaml
|jedai| has quit [Connection timed out]
altmattr has left #ocaml []
|jedai| has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
_jedai_ has quit [Read error: 110 (Connection timed out)]
Camarade_Tux has joined #ocaml
jeremiah has joined #ocaml
mrchebas has quit ["Leaving"]
jeremiah has quit [Read error: 104 (Connection reset by peer)]
s4tan has joined #ocaml
jeremiah has joined #ocaml
OChameau has joined #ocaml
marmotine has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
tiremeal has joined #ocaml
jknick has quit ["leaving"]
rwmjones_ has joined #ocaml
realtime has quit [Read error: 145 (Connection timed out)]
pierre- has joined #ocaml
jeremiah has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
Axioplase has quit ["brb"]
jeremiah has joined #ocaml
rwmjones_ has quit ["Closed connection"]
jeremiah has quit [Read error: 104 (Connection reset by peer)]
_zack has joined #ocaml
Axioplase has joined #ocaml
realtime has joined #ocaml
jeremiah has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
vixey has joined #ocaml
tiremeal has quit [Connection timed out]
jeremiah has joined #ocaml
tiremeal has joined #ocaml
tiremeal has quit [Client Quit]
realtime has quit [Connection timed out]
pango has quit [Remote closed the connection]
pango has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
jeremiah has joined #ocaml
jeremiah has quit [Connection reset by peer]
fschwidom has joined #ocaml
sgnb has quit [Read error: 104 (Connection reset by peer)]
Snark has joined #ocaml
jeremiah has joined #ocaml
Associat0r has joined #ocaml
sgnb has joined #ocaml
smimram has quit ["bli"]
smimou has joined #ocaml
itewsh has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
hkBst has joined #ocaml
itewsh has quit ["There are only 10 kinds of people: those who understand binary and those who don't"]
sporkmonger has joined #ocaml
|jeremiah has joined #ocaml
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
itewsh has joined #ocaml
|jeremiah has joined #ocaml
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
|jeremiah has joined #ocaml
fschwidom has quit [Remote closed the connection]
pierre- has quit [Read error: 110 (Connection timed out)]
schme has joined #ocaml
itewsh has quit ["There are only 10 kinds of people: those who understand binary and those who don't"]
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
vixey has quit [Remote closed the connection]
|jeremiah has joined #ocaml
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
smimram has joined #ocaml
hcarty has quit [Read error: 104 (Connection reset by peer)]
pierre- has joined #ocaml
ched has joined #ocaml
pango has quit [Remote closed the connection]
|jeremiah has joined #ocaml
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
hcarty has joined #ocaml
mishok13 has quit [Read error: 60 (Operation timed out)]
smimou has quit [Read error: 110 (Connection timed out)]
pango has joined #ocaml
_zack has left #ocaml []
|jeremiah has joined #ocaml
|jeremiah has quit [Success]
mishok13 has joined #ocaml
jeremiah has joined #ocaml
<rwmjones>
_zack, ping
s4tan has quit []
jeremiah has quit [Read error: 104 (Connection reset by peer)]
jeremiah has joined #ocaml
Strst-prst-mrck has joined #ocaml
Strst-prst-mrck has left #ocaml []
jeremiah has quit [Read error: 104 (Connection reset by peer)]
fschwidom has joined #ocaml
vixey has joined #ocaml
jeremiah has joined #ocaml
_zack has joined #ocaml
jlouis has quit [Remote closed the connection]
jlouis has joined #ocaml
pango has quit [Remote closed the connection]
pango has joined #ocaml
ikaros has joined #ocaml
OChameau has quit ["Leaving"]
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
middayc has joined #ocaml
|jedai| has quit [Read error: 60 (Operation timed out)]
ygrek has joined #ocaml
|jedai| has joined #ocaml
ygrek has quit [Remote closed the connection]
ikaros has quit [Read error: 60 (Operation timed out)]
Pound_Sterling has joined #ocaml
ikaros has joined #ocaml
Pound_Sterling has left #ocaml []
dirtyd has joined #ocaml
ygrek has joined #ocaml
etate has joined #ocaml
|jedai| has quit [Connection timed out]
|jedai| has joined #ocaml
seafood has joined #ocaml
ikaros has quit [".quit"]
|jedai| has quit [Operation timed out]
|jedai| has joined #ocaml
|jedai| has quit [Read error: 145 (Connection timed out)]
|jedai| has joined #ocaml
fschwidom has quit [Connection timed out]
Yoric[DT] has joined #ocaml
<Yoric[DT]>
hi again
<kig>
anyone know of a good guide to developing software with the aid of a proof assistant?
<kig>
Yoric[DT]: hi
<Yoric[DT]>
No but if you find one, I'd be interested.
<thelema>
kig: what would you want the proof assistant to do?
<thelema>
I hope you don't say "proving" that something "works"
<kig>
i don't know, that's why i'm asking :|
<mrvn>
thelema: why not?
<kig>
or, how does one develop high-integrity software in practice
<mrvn>
kig: patiently :)
<mrvn>
If you write your interfaces nicely and add some restrains you can even proof that the function do what the interface/restrains say it should.
<thelema>
mrvn: every program "works" in a sense (maybe as long as it compiles). But whether it "does what I want" can't be proven without a formal description of "what I want"
<mrvn>
thelema: that is where I would think the "aid" part comes in.
<mrvn>
aiding in writing constrains and formalizing what one wants it to do.
<thelema>
proof assistants don't seem the right tool to formalize intent.
seafood has quit []
<kig>
you can use coq to write functions and prove things about them (and extract ocaml/haskell code), but you need to figure out what you can and should prove about it. so a guide that talks about that would be nice
<thelema>
especially since most programmers learn what they really meant in the first place as part of the process of explaining to a computer how to do something.
<Yoric[DT]>
kig: you should take a look at Focal.
Associat0r has quit []
pierre- has quit [Read error: 145 (Connection timed out)]
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
dirtyd has left #ocaml []
<kig>
Yoric[DT]: thanks, looking
<kig>
zzz ->
Snark has quit ["Ex-Chat"]
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
seafood has joined #ocaml
Palace_Chan has joined #ocaml
sporkmonger has quit [Read error: 110 (Connection timed out)]
tvn has joined #ocaml
<tvn>
hi all, if I call my program like this ./prog -f something -b -3 -s , how can I store this call ? -- that is I want to know exactly what passed in the program in the run , so storing the entire "./prog -f something -b -3 -s" as string
<tvn>
I don't think Arg has something to suppor this ?
<brendan>
it's in Sys.argv
etate has quit [Read error: 104 (Connection reset by peer)]
sporkmonger has joined #ocaml
_zack has quit ["Leaving."]
<tvn>
thank you
_jedai_ has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
marmotine has quit ["mv marmotine Laurie"]
hkBst has quit [Read error: 104 (Connection reset by peer)]
_jedai_ has quit [Connection timed out]
|jedai| has joined #ocaml
_zack has joined #ocaml
_zack has quit [Client Quit]
slash_ has joined #ocaml
thelema has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Read error: 110 (Connection timed out)]
comglz has joined #ocaml
|jedai| has joined #ocaml
|jedai| has quit [Read error: 145 (Connection timed out)]
|jedai| has joined #ocaml
ygrek has quit [Remote closed the connection]
ygrek has joined #ocaml
Mr_Awesome has quit ["aunt jemima is the devil!"]
_jedai_ has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
Associat0r has joined #ocaml
Demitar has quit [Remote closed the connection]
ygrek has quit [Remote closed the connection]
vixey has quit [Remote closed the connection]
Amorphous has quit [Read error: 110 (Connection timed out)]