Drup has quit [Read error: Connection reset by peer]
Drup has joined #ocaml
ollehar has joined #ocaml
dsheets has quit [Quit: Leaving]
darkf has joined #ocaml
oriba has quit [Quit: oriba]
madroach has quit [Ping timeout: 264 seconds]
madroach has joined #ocaml
cthuluh has joined #ocaml
Drup has quit [Quit: Leaving.]
carleastlund has quit [Quit: carleastlund]
q66 has quit [Quit: Leaving]
ben_zen has joined #ocaml
ygrek has joined #ocaml
Neros has quit [Read error: Operation timed out]
ollehar has quit [Ping timeout: 256 seconds]
walter|r has joined #ocaml
ygrek has quit [Ping timeout: 268 seconds]
ygrek has joined #ocaml
csakatoku has joined #ocaml
ggole has joined #ocaml
walter|r has quit [Read error: Connection reset by peer]
walter has joined #ocaml
zpe has joined #ocaml
Xom has quit [Read error: Connection reset by peer]
Xom has joined #ocaml
zpe has quit [Ping timeout: 248 seconds]
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
cdidd has quit [Remote host closed the connection]
zpe has joined #ocaml
cdidd has joined #ocaml
Simn has joined #ocaml
vpit3833` has joined #ocaml
zpe has quit [Ping timeout: 256 seconds]
vpit3833 has quit [Disconnected by services]
vpit3833` is now known as vpit3833
zarus has joined #ocaml
weie has quit [Quit: Leaving...]
zpe has joined #ocaml
ygrek has quit [Ping timeout: 246 seconds]
zpe has quit [Ping timeout: 268 seconds]
zarus has quit [Quit: Leaving]
dsheets has joined #ocaml
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
zpe has joined #ocaml
zRecursive has left #ocaml []
hkBst has joined #ocaml
osa1 has joined #ocaml
mcclurmc has joined #ocaml
csakatok_ has joined #ocaml
zpe has quit [Ping timeout: 268 seconds]
csakatoku has quit [Ping timeout: 276 seconds]
thomasga has joined #ocaml
Yoric has joined #ocaml
ygrek has joined #ocaml
mika1 has joined #ocaml
AltGr has joined #ocaml
ben_zen has quit [Ping timeout: 248 seconds]
Yoric has quit [Ping timeout: 246 seconds]
walter has quit [Read error: Connection reset by peer]
gnuvince has quit [Read error: No route to host]
walter has joined #ocaml
djcoin has joined #ocaml
zpe has joined #ocaml
zpe has quit [Ping timeout: 255 seconds]
zpe has joined #ocaml
librarian has joined #ocaml
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
Snark has joined #ocaml
eikke has joined #ocaml
tianon has quit [Read error: Operation timed out]
tianon has joined #ocaml
zarus has joined #ocaml
<gasche>
whitequark: you may consider writing a sublime frontend for Merlin
<gasche>
(or getting someone to write one :)
<gasche>
I don't like closed-source programming tools, but I think having more frontend can only improve Merlin's design
Kakadu has joined #ocaml
weie has joined #ocaml
<zarus>
I'm just wondering: what would #ocaml think of a unix clone written in o?caml? What would be the advantages/disadvantages of this
walter has quit [Read error: Connection reset by peer]
zarus has quit [Quit: Leaving]
mcclurmc has quit [Quit: Leaving.]
<gasche>
that unix clone idea disappeared too fast...
walter has joined #ocaml
<ousado>
lol
<ousado>
hm mirage counts as one.
<fds>
I'd be interested in hearing the answer too, although my gut reaction is that it would be completely pointless NIHing and if one were to write an OS in OCaml, it could do better than being a Unix clone. ;-)
<gasche>
well
<companion_cube>
hi there
<gasche>
there was a hobby project to write a kernel using OCaml, like ten years ago
<gasche>
iirc. it was called Spring
<gasche>
it fell into dust when the students that had teamed to do that went in different directions, I guess
<gasche>
it's hard to remain motivated on such lone rangers projects
<gasche>
ousado: I'd say Mirage counts, indeed
<gasche>
there was also a microkernel project, Coyotos, that design its own system programming language with strong ML roots, but it was abandoned after some time
<Kakadu>
gasche: hi!
ocp has joined #ocaml
<Kakadu>
I realised more concretely my Friday's issue . It was not parsing combintors corrupting memeory: it was ocamllex lexing phase doing it.
<gasche>
"corrupting", you're a bit too strong :)
<Kakadu>
)
ontologiae has joined #ocaml
librarian has left #ocaml []
walter has quit [Read error: Connection reset by peer]
<ousado>
If I had some additional 48 hours per day and had to write an OS, ATS would be a strong candidate for the low level stuff
walter has joined #ocaml
<ousado>
s/ATS would be/I'd consider ATS as
<gasche>
indeed
<gasche>
Rust is becoming interesting as well, and has more traction, but the design process is a bit too messy
<gasche>
(Rust was interesting from the start, I'm meaning he's becoming more usable)
<ggole>
Does ocamllex allocate a buffer for each lexeme even if such is not used?
<Kakadu>
Rust which is mozilla's Rust?
<Kakadu>
ggole: lexbuf is not allocated. it is mutable
<ggole>
I see, so getting the lexeme is a copy.
<ggole>
That makes sense.
<ggole>
I got interested in writing fast lexers a while back, so this is idle curiosity.
<Kakadu>
btw,
<Kakadu>
Can somebody point a link about GADTs and parser-combinators?
<def-lkb>
rust were interesting when they considered tailrec… and now with their T<A> syntax to introduce parametricity, it looks more like C++ than like a usable language
<gasche>
to be fair
<def-lkb>
was*
<gasche>
it's hard to get something pretty when you start from the ML syntax
yacks has quit [Read error: Connection reset by peer]
<gasche>
(AST has a bit of the same issue)
<def-lkb>
… and putting java/c++ into the playground is an obvious improvement
<gasche>
I'm not sure that's a problem when you actually use the language, though
<ggole>
If Rust turns out to be an ugly but safe low-level language, it can still be worthwhile.
* def-lkb
is just trolling
thomasga has quit [Quit: Leaving.]
thomasga has joined #ocaml
<gasche>
to be fair, ATS is not pretty
<gasche>
I think when you move into that design space, its natural that the language design feels cluttered
<gasche>
you can try to do better than C++ but ultimately you face some of the same issues
<gasche>
things could probably be simplified, but we'll only see it in retrospect
<ggole>
It's a lot easier to look nice if you don't have pointers.
<def-lkb>
what makes you think this design space is that hard ?
<gasche>
(for example, not having mutable *variables* is one of the things that simplifies ML's design as opposed to most imperative languages)
<def-lkb>
C is relatively clean
<gasche>
but C is not safe
<def-lkb>
(you have a point with mutable variables!)
<ggole>
Safe pointer types always seem to end being cluttery.
<gasche>
in ML implementations, there is a correlation between the base unit of mutability, references, and heap-boxed data
<gasche>
that makes it look unsuitable for systemish purposes
<gasche>
but you can separate the two, and have a lower-level notion of mutable data that is not heap-boxed
<gasche>
(I think Harper's book does some of that)
<ggole>
Javascript does some of that.
<gasche>
while still having the nice property of being a (r)value and not something magical about variable naming
<ggole>
Apparently there are suggestions to add "real" structs too
<ggole>
Not just typed arrays
<ggole>
And the Java guys want layout control too
mcclurmc has joined #ocaml
<ggole>
I wonder how they intend to deal with the consequences of that approach. Direct data representations might cause trouble for GC.
<gasche>
with lots of people and money :-'
<ggole>
The Lisp machine guys had an approach called 'locatives' to deal with pointers to the middle of objects, back in the day
<ggole>
IIRC it was backed by hardware support.
ocp has quit [Ping timeout: 260 seconds]
<ggole>
I think that's what you need for layout control.
<def-lkb>
I am not sure it really makes sense to mix low-level & gc in the same language
<def-lkb>
(Rust got this right with their optionnaly garbage-collected tasks)
<ousado>
there are sml implementations that do fine
<ousado>
if you count region-inference as low-level
<ggole>
How do they deal with relocation of objects that are pointed-to in the middle?
<ggole>
You could use fat pointers, but that would get expensive pretty fast.
<ousado>
hm, if you want the details I'll have to look up the paper
<ggole>
You could eliminate relocation for such objects (while keeping it for others), but GC might become too slow.
<companion_cube>
rust looks like they're drifting away from the GC
<ousado>
ML Kit
<ggole>
I'll have a look, thanks.
<def-lkb>
ousado: by low-level I was thinking of mapping hardware registers, that expect a specific representation
<companion_cube>
more and more toward unique pointers everywhere
<ousado>
def-lkb: IIRC sgen deals with register
<ousado>
s
<ousado>
the new mono gc
yacks has joined #ocaml
<ousado>
there are some quite in-depth posts about its architecture
<def-lkb>
ousado: i was thinking about descriptor tables… and yes it is definitely possible to make a GC run into such condition
<def-lkb>
(if any, the Boehm conservative one)
Matthieu3 has joined #ocaml
<def-lkb>
it's just that the context in which you have to deal with hardware registers seems inappropriate for GC'ed tasks
<ggole>
That's not the only low-level concern.
<ggole>
Often you want to align things to cache-lines or use vector-friendly representations
<ggole>
("Often". Sometimes.)
<ggole>
ousado: the relevance of the paper seems to be that if the lifetime of a structure is just right, you don't need to do any GC at all. Is that right?
<ggole>
If so, I don't think that's a substitute for solving the problem in the general case.
walter|r has joined #ocaml
ollehar has joined #ocaml
ocp has joined #ocaml
walter has quit [Ping timeout: 248 seconds]
<ousado>
ggole: actually mixing in the GC isn't necessary
Matthieu5 has joined #ocaml
<ousado>
they just wanted to see how it works out
<ousado>
the main point of mixing them is to reduce pressure on the GC
Matthieu6 has joined #ocaml
Matthieu7 has joined #ocaml
Matthieu5 has quit [Ping timeout: 276 seconds]
Matthieu3 has quit [Ping timeout: 276 seconds]
yacks has quit [Ping timeout: 246 seconds]
yacks has joined #ocaml
Yoric has joined #ocaml
ocp has quit [Ping timeout: 248 seconds]
<whitequark>
gasche: I've looked at Merlin; it seems rather enormous for me
<whitequark>
that's not necessarily bad, but the ocp-index plugin I've hacked in two days and it works rather well. it's a 80% solution, indeed.
Yoric has quit [Ping timeout: 264 seconds]
walter has joined #ocaml
ontologiae has quit [Ping timeout: 248 seconds]
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
walter|r has quit [Ping timeout: 276 seconds]
yacks has quit [Ping timeout: 240 seconds]
yacks has joined #ocaml
<mrvn>
AMD does cover it.
<mrvn>
ups
cdidd has quit [Remote host closed the connection]
cdidd has joined #ocaml
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
cdidd has quit [Remote host closed the connection]
Neros has joined #ocaml
cdidd has joined #ocaml
q66 has joined #ocaml
thomasga has quit [Quit: Leaving.]
thomasga has joined #ocaml
mfp has joined #ocaml
csakatok_ has quit [Remote host closed the connection]
_andre has joined #ocaml
ygrek has quit [Ping timeout: 264 seconds]
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
osa1 has quit [Ping timeout: 276 seconds]
osa1 has joined #ocaml
Drup has joined #ocaml
osa1 has quit [Ping timeout: 240 seconds]
yacks has quit [Ping timeout: 260 seconds]
ontologiae has joined #ocaml
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
yacks has joined #ocaml
<Kakadu>
If we will lok at manual about Lexing.lexbuf structure we'll see that some fields of this structure and not described. Is it an issue to be reported?
<AltGr>
Kakadu: guess the best documentation in this case is the source
fantasticsid has joined #ocaml
<kerneis>
well, it does say the other fields are left unchanged
<kerneis>
the question is indeed what they might be used for
<kerneis>
hmm, even refill_buff is not documented
n06rin has joined #ocaml
walter has quit [Read error: Connection reset by peer]
n06rin1 has joined #ocaml
walter has joined #ocaml
n06rin has quit [Ping timeout: 268 seconds]
gnuvince has joined #ocaml
gnuvince has quit [Changing host]
gnuvince has joined #ocaml
tobiasBora has joined #ocaml
fantasticsid has quit [Remote host closed the connection]
<tobiasBora>
Hello,
<kerneis>
hi
<tobiasBora>
I'm trying to use OpenGl with the liblablGL but I've problems with 3D : I can't change the camera orientation !
smondet has joined #ocaml
<tobiasBora>
I tried GluMat.look_at ~eye:(1., 1., 1.) ~center:(0., 0., 0.) ~up:(0., 0., 1.); but nothing appear, I've only a green screen
<adrien_>
ah, I knew it: ocamlbuild implements cp through a call to the "cp" binary
<kerneis>
I rely on cp anyway in many places
<kerneis>
I even rely on configure and gnu make
<adrien_>
yeah, sure, but calls to external commands in ocamlbuild is a real pain =/
ben_zen has quit [Ping timeout: 245 seconds]
<kerneis>
anyway, it still doesn't work because ocamlbuild is so smart it detects a circular dependency
<kerneis>
hmmm hmmmm hmmmm
<kerneis>
I think I'll give up on this whole natdynlink plan, and only support bytecode from now on
<kerneis>
who cares about efficiency anyway?
<adrien_>
on which platforms does it not work?
<n06rin>
AAAAAA I read real world ocaml book, but now authors denied access to me. I'm really sad. Try to write one of the authors, maybe it take me access
<n06rin>
oh, i see. I read beta2 but you open beta3, lol
adrien_ is now known as adrien
<n06rin>
gasche: thanks a lot. Maybe later i will read books from this advices.
<n06rin>
But now I want concentrate on real world ocaml
<gasche>
it's fine
<gasche>
it doesn't actually makes much sense to read another "beginner book" after that
<gasche>
there are more advanced books that may still be of interest, though
<gasche>
(eg. U3-OCaml)
ygrek has joined #ocaml
zarus has joined #ocaml
<kerneis>
gasche: do you know what the status of ocambuild under windows is?
<gasche>
it works
<kerneis>
good, then I can slap my colleague in the face with a large trout
<kerneis>
thanks
<gasche>
the original authors took great care of having the "degraded mode" where not all the nice unix things we're used to are available
<gasche>
it won't be as good as on Unix, though
<kerneis>
no problem
<gasche>
it's sensibly slower because it uses Cygwin's bash or something like that, and I suspect it doesn't parallelize at all -- not that the Unix version does a great job either
<thomasga>
kerneis: it works but it's terribly slow
<adrien>
I wouldn't call it "terribly" slow
<adrien>
it's definitely slower
<kerneis>
I couldn't care less about efficiency
<gasche>
there has been some discussion of how to make some of that overhead go away
<thomasga>
and timestamps have a 1s precision
<kerneis>
I just need something correct
<adrien>
but it's not slower than compiling C++
<thomasga>
so you will often recompile everything
<gasche>
between adrien and william on the bugtracker
<kerneis>
I will never develop on windows
<thomasga>
but yup, it works
<gasche>
PR#5201
<kerneis>
I want my users to be able to compile on it, that's all
<gasche>
if people are interested in contributing, that's fine
<gasche>
kerneis: I think the WODI guy had a good story about that
<adrien>
well, just stop using Unix.open_process* in ocamlbuild :P
Neros has quit [Ping timeout: 245 seconds]
<gasche>
like projects using ocamlbuild (and maybe omake?) working mostly out of the box on windows
<pippijn>
"A dynamically loaded C DLL can refer to any symbol from the main program (symbols of the caml runtime, or symbols of statically-linked C code) and to any symbol from a previously loaded C DLL. The dllimport/dllexport declspecs modifiers in the C code are no longer needed."
<pippijn>
I wonder how that works
hkBst has quit [Quit: Konversation terminated!]
mcclurmc has quit [Quit: Leaving.]
mika1 has quit [Quit: Leaving.]
<levi>
Magic!
<levi>
Linking is a bit of a black art, especially dynamic linking.
<gasche>
pippijn: re. your message error technique, I looked a bit at what was available for LR parsers and I saw something very similar to what you're doing in a Russ Cox article about reimplementing in Go something that was already known
<gasche>
(I'm not sure whether you know about this related work, which is why I'm citing it here)
<pippijn>
gasche: I don't know about it, yet
mcclurmc has joined #ocaml
<gasche>
I read about another error-reporting technique from John Shutt of LtU
<gasche>
which is not about the message itself but the location reported
<gasche>
he advises to highlight the "smallest non-trivial incomplete expression"
<gasche>
(instead of just the point where the parser gives up)
<pippijn>
that's interesting
<gasche>
it's a bit unclear to me what the precise definition for this is in the general case
walter has quit [Quit: This computer has gone to sleep]
<gasche>
but I've been running examples in my head and it looks rather nice
<companion_cube>
do you run them in bytecode or native code?
<gasche>
I'm wondering how to implement that in the context of a LR parser generator
<gasche>
companion_cube: if you allow me to get slightly off-topic, I think the habit of running code in one's head is the main difference between people that get programming, and those that feel they'll never understand it
<gasche>
(I'm not saying that there is a clear divide between those two groups, but rather than the most important thing to tell someone to avoid getting him in the second is to run code in his/her head, with a piece of paper to write down the steps)
<gasche>
I'll get a fresh batch of L1 students to test this in real conditions in about a month
<companion_cube>
I was just joking ^^
<gasche>
the only problem is that they're supposed to be taught Java
<gasche>
I have no idea how to run Java code in one's head :-'
<mathieui>
gasche: it ends badly
Yoric has joined #ocaml
yacks has joined #ocaml
Yoric has quit [Ping timeout: 245 seconds]
skchrko has quit [Quit: Leaving]
weie has quit [Read error: Connection reset by peer]
weie has joined #ocaml
zarus has quit [Ping timeout: 245 seconds]
jbrown has quit [Ping timeout: 248 seconds]
zarus has joined #ocaml
ontologiae has quit [Ping timeout: 268 seconds]
watermind has joined #ocaml
<watermind>
just to make sure... records types always have to be declared right?
<watermind>
i.e. it is not possible to return a record unless the corresponding record type has been explecitely declared before
<Drup>
watermind: yes
<watermind>
Drup: much like there are polymorphic variants I thought there may be something similar for product types
<Drup>
there is : objects
<watermind>
where oh
<watermind>
don't want to get into that just yet...
Kakadu has quit [Quit: Konversation terminated!]
<ggole>
let whee () = object method x = 1 end
<Drup>
it's not really as terrible as it sound :p
zarus has quit [Ping timeout: 248 seconds]
zarus has joined #ocaml
darkf has quit [Quit: Leaving]
<watermind>
probably, but still getting used to the syntax and getting to know the module system
<watermind>
so... one step at a time
jbrown has joined #ocaml
<ggole>
You can also use tuples, I guess
<ggole>
Although they aren't a great idea once you get more than two or three elements.
mcclurmc has quit [Quit: Leaving.]
<watermind>
ggole: yes but labels are really handy to not accidentally mix positions
AltGr has quit [Quit: Konversation terminated!]
<ggole>
Labels are great. They won't help destructuring though.
<watermind>
they don't? isn't that what pattern match does?
<watermind>
or maybe I'm missinterpreting "destructuring"
<watermind>
is that the same as deconstructing or something else?
tane has joined #ocaml
<ggole>
Well, let a, b, c = some_tuple in ...
<ggole>
There are no labels there.
<ggole>
You can use them in construction by writing a "smart constructor", let foo ~x ~y ~z = x, y, z
<pippijn>
let { a; b; c; } = some_record in ...
ben_zen has joined #ocaml
<ggole>
But it would be better to just use a record
n06rin has quit [Quit: Leaving.]
<Drup>
I think ggole is talking about function labels and watermind about record fields
<ggole>
At least half right :)
<watermind>
oh
ben_zen has quit [Ping timeout: 264 seconds]
zarus has quit [Ping timeout: 276 seconds]
zarus has joined #ocaml
<watermind>
is there anything like frama-c for ocaml?
zpe has quit [Remote host closed the connection]
<watermind>
particularly to define specifications and automatically-theorem-prove them
<ggole>
Coq, maybe
<watermind>
I know Coq is written in OCaml, but is there any integration between both?
<ggole>
There is automatic extraction from Coq to OCaml, I believe.
<watermind>
right
<watermind>
that's interesting
<watermind>
got to look at it
<watermind>
I was thinking something a bit different though, which is given OCaml code, be able to add specifications/assertions in comments, to be proved with some static verification system
chambart has joined #ocaml
<ggole>
I don't know of any such tool.
<mrvn>
Express them as types.
chambart has quit [Ping timeout: 248 seconds]
<watermind>
mrvn: types, particularly in ocaml, don't let you express that much
<Drup>
watermind: depends, what do you want to express ?
<mrvn>
with gadts you get a bit further than before
<watermind>
mrvn: even haskell with it's initial "dependent type"-like support doesn't give you much
<watermind>
still
<watermind>
"this array will end up sorted"
<ggole>
You can use phantom types to track certain kinds of properties
<ggole>
There is nothing automatic about it, though.
<watermind>
I know I do all that, it is quite useful to aid correct development of programs
<watermind>
but it's different from strong static verification
<mrvn>
watermind: you can at least garanty that the sorting remains within the bounds of an array so you can use the faster unsafe_get method.
Yoric has joined #ocaml
<ggole>
Yes, it's not model checking.
<watermind>
true
<watermind>
there's quite a bit one can do
<mrvn>
checking that the result is actualy sorted is hard. How would you even specify that? \forall i,j with i < j: x.(i) < x.(j)?
<watermind>
well x.(i)<=x.(j) but yes
<mrvn>
I think that would require symbolic execution of the code to check.
<watermind>
not really...
<watermind>
unless you have something in mind I'm not considering
<watermind>
it's a basic/intermediate exercise using e.g. acsl (frama-c) or in a dependently typed language like agda
<watermind>
assuming you do it imperatively, with loops and assignments the proof can be done with Hoare's axiomatic, which is what ACSL is based on
<mrvn>
well, in ocaml you would have recursion and folding and such
<watermind>
if you use recursion then the proof is by induction
<watermind>
which is even easyer
<watermind>
easier*
<watermind>
note I'm not expecting a system where you'd just give the assertion and it automatically proves it
<watermind>
instead you'd guide the proof, with the automation being used only to get rid of boilerplate
Yoric has quit [Ping timeout: 246 seconds]
ygrek has quit [Ping timeout: 264 seconds]
csakatoku has quit [Remote host closed the connection]
<companion_cube>
< watermind> I was thinking something a bit different though, which is given OCaml code, be able to add specifications/assertions in comments, to be proved with some static verification system <--- why3.
<ggole>
\forall i,j with i < j: x.(i) <= x.(j) isn't hard to meet: for i = 0 to Array.length a - 1 do a.(i) <- a.(0) done
<mrvn>
I would find that rather useless. Then I have to manualy guide the proof every time I change something in the source.
<companion_cube>
just look at this and enjoy
<mrvn>
ggole: That would be a runtime assertion. We were talking static, as in compile time, assertion.
<watermind>
companion_cube: oh!!!
<watermind>
companion_cube: I didn't know that
<mrvn>
ggole: oh wait, you ment that as (buggy) implementation of sort?
Drup has quit [Ping timeout: 245 seconds]
<ggole>
I meant that it would satisfy the predicate, but it is (obviously) not a sort.
<watermind>
companion_cube: i.e. I know why3 and (implicitely) use it in frama-c as one of the provers, but I didn't know about whyML
<companion_cube>
watermind: you still have to write induction proofs in coq, I think, because alt-ergo (the theorem prover) cannot do them
<companion_cube>
watermind: it's arrived in why3
<companion_cube>
it's OCaml + annotations, just as you wanted ^^
<mrvn>
ggole: yeah, even defining just what sort is is not easy. At least I don't know how you would say that every element in the input must appear in the output exactly once.
<companion_cube>
ggole: you also have to specify it's a permutation of the input
<ggole>
Theorem provers can do that sort of thing: I found them difficult to approach though.
<watermind>
companion_cube: hmm... still a bit confused about how this ecosystem works. So WhyML is the specification language, Why3 a theorem prover... where does alt-ergo fit here? I thought alt-ergo was just another theorem prover
<companion_cube>
whyML is a language that compiles to ML, and also to proof obligations in why3's logic
<watermind>
right
<companion_cube>
why3 proof obligations can be sent to theorem provers
<watermind>
oh
<companion_cube>
among which coq (for hard proofs), and alt-ergo for easy ones
<watermind>
I see gotcha
<watermind>
right, so this is indeed what I was looking for
<watermind>
it seems
<watermind>
ah I just realised I was confusing Why3 with Microsofts' Z3 the latter being a theorem prover
zarus has quit [Ping timeout: 264 seconds]
<watermind>
frama-c, which is for C, uses ACSL for the specification language and also translates it to the Why3 as the logic, so I'm guessing maybe all those theorem provers can be used with the programs generated by WhyML
<watermind>
got to look at this more closely... thanks companion_cube!
tobiasBora has quit [Ping timeout: 246 seconds]
zarus has joined #ocaml
Yoric has joined #ocaml
zpe has joined #ocaml
zpe has quit [Ping timeout: 264 seconds]
Yoric has quit [Ping timeout: 264 seconds]
ulfdoz has joined #ocaml
Yoric has joined #ocaml
ocp has joined #ocaml
Yoric has quit [Ping timeout: 246 seconds]
zarus has quit [Ping timeout: 256 seconds]
zarus has joined #ocaml
ocp has quit [Ping timeout: 246 seconds]
Drup has joined #ocaml
Drup has quit [Client Quit]
Drup has joined #ocaml
csakatoku has joined #ocaml
Drup1 has joined #ocaml
Drup has quit [Ping timeout: 264 seconds]
csakatoku has quit [Ping timeout: 260 seconds]
Matthieu7 has quit [Quit: Leaving.]
Matthieu2 has joined #ocaml
tane has quit [Quit: Verlassend]
gnuvince has quit [Remote host closed the connection]
ben_zen has joined #ocaml
Drup1 has quit [Ping timeout: 276 seconds]
ben_zen has quit [Ping timeout: 248 seconds]
ggole has quit []
zarus has quit [Ping timeout: 245 seconds]
Neros has joined #ocaml
malo has joined #ocaml
Yoric has joined #ocaml
Yoric has quit [Ping timeout: 246 seconds]
Matthieu2 has quit [Read error: Connection reset by peer]
Matthieu2 has joined #ocaml
zarus has joined #ocaml
Yoric has joined #ocaml
pkrnj has joined #ocaml
Fullma has quit [Ping timeout: 256 seconds]
Matthieu2 has left #ocaml []
Fullma has joined #ocaml
Yoric has quit [Ping timeout: 258 seconds]
yacks has quit [Ping timeout: 264 seconds]
Snark has quit [Quit: leaving]
Fullma has quit [Ping timeout: 256 seconds]
chambart has joined #ocaml
zarus has quit [Ping timeout: 264 seconds]
<levi>
Coq is fun if you have a guided intro to it.
<levi>
It's kind of like playing sudoku or something.
<levi>
After learning a bit of Coq, I thought it would be a fun project to 'gamify' doing simple formal proofs in a theorem proving system.
<companion_cube>
some people write real code in coq
Yoric has joined #ocaml
_andre has quit [Quit: leaving]
zarus has joined #ocaml
gnuvince has joined #ocaml
gnuvince has quit [Changing host]
gnuvince has joined #ocaml
<levi>
Sure, the projection tools it provides are nifty, though I never got to the point of playing with them.
<levi>
I just found it surprisingly fun to play with even though I didn't have anything 'real' to do with it.
Yoric has quit [Ping timeout: 246 seconds]
Matthieu6 has left #ocaml []
Yoric has joined #ocaml
ben_zen has joined #ocaml
Anarchos has joined #ocaml
ben_zen has quit [Ping timeout: 245 seconds]
<Anarchos>
how do i invoke ocamldoc from ocamlbuild ?
<def-lkb>
levi: I had exactly the same impression
zarus has quit [Ping timeout: 248 seconds]
<companion_cube>
Anarchos: write a .odocl file
zarus has joined #ocaml
ocp has joined #ocaml
Yoric has quit [Ping timeout: 246 seconds]
tobiasBora has joined #ocaml
<whitequark>
why doesn't partial application in ocaml produce strongly polymorphic functions?
<whitequark>
just to simplify the core language, since this case is rare and easily worked around?
<watermind>
when trying to install coq via opam I get: Application of .opam/4.00.1/build/coq.8.4pl2/CAML_LD_LIBRARY_PATH.patch failed: can not determine the correct patch level.
<bungley>
it doesn't?
<watermind>
any idea how to approach this?
Yoric has joined #ocaml
<whitequark>
bungley: utop # List.map (fun x -> x);;
<whitequark>
- : '_a list -> '_a list = <fun>
<whitequark>
cf. (fun l -> List.map (fun x -> x) l) : 'a list -> 'a list
<def-lkb>
that would be unsafe whitequark
<whitequark>
def-lkb: why?
<whitequark>
aren't the two statements above equivalent?
<def-lkb>
e.g. let f () = let r = ref None in fun x -> let result = !r in r := (Some x); result
<def-lkb>
if f' was strongly polymorphic, e.g f' : 'a -> 'a option
<def-lkb>
then ignore (f' "hello"); f' 1 would return the value (Some "hello") with type int option
<whitequark>
def-lkb: oh I think I understand: while in a common case with a function with e.g. two arguments applying it to one won't execute anything, this is not necessarily true
<bungley>
what's the difference between "'a list -> 'a list = <fun> " and " '_a list -> '_a list = <fun> "?
<whitequark>
def-lkb: and you can have a function which after first application does something with a side effect, which would make polymorphism unsound in that case
<def-lkb>
whitequark: exactly
<whitequark>
thanks
<whitequark>
bungley: see rks`'s link
<bungley>
ah, thanks
ulfdoz has quit [Ping timeout: 264 seconds]
ddonna has quit [Quit: Lost terminal]
<companion_cube>
who was interested in IndexedSet here?
<watermind>
companion_cube: was looking at WhyML, seems pretty cool... it does however differ a bit from Frama-C/WP/ACSL for C, or for instance
<watermind>
in the sense that when using the latter you actually write a C program, and the specification in ACSL is in the comments of your program
<watermind>
then this gets translated to Why (WhyML?)
<watermind>
when using WhyML directly however you're not really coding OCaml. The programming language in WhyML is simply ML like, and apparently you can generate OCaml code form it
<watermind>
so it's kind of the reverse
<def-lkb>
:qa
<def-lkb>
oops, sorry
<watermind>
it is pretty cool... but it's a shame that a bunch of tools are built to use Why3 for other languages directly (C, Ada...) but not for OCaml
beginnner42 has joined #ocaml
<beginnner42>
dsheets: hi
<beginnner42>
did you have a look at the repository?
Yoric has quit [Ping timeout: 246 seconds]
malo has quit [Quit: Leaving]
Drup has joined #ocaml
thomasga has quit [Quit: Leaving.]
Yoric has joined #ocaml
Yoric has quit [Ping timeout: 246 seconds]
Yoric has joined #ocaml
Simn has quit [Quit: Leaving]
csakatoku has joined #ocaml
chambart has quit [Ping timeout: 246 seconds]
Yoric has quit [Ping timeout: 246 seconds]
Yoric has joined #ocaml
osa1 has joined #ocaml
csakatoku has quit [Ping timeout: 260 seconds]
Yoric has quit [Ping timeout: 246 seconds]
ocp has joined #ocaml
<watermind>
I'm trying to compile coq and it complains it can't find dlllablgtk2.so - however I do have it in .opam/4.00.1/lib/stublibs
<watermind>
any ideas?
beginnner42 has quit [Quit: Leaving]
ocp has quit [Ping timeout: 260 seconds]
<Anarchos>
watermind compile without gtk support ?
<watermind>
Anarchos: I'd like gtk support though, I do have lablgtk2 installed and it even finds the dir during ./configure
<Anarchos>
as i work on a platform without gtk, i can't help you !
<watermind>
:/
zRecursive has joined #ocaml
eikke has quit [Ping timeout: 260 seconds]
gnuvince has quit [Remote host closed the connection]