<watermind>
quite a change to see a fold_right implemented by reversing the list first and then applying a fold_left
lusory has quit [Ping timeout: 240 seconds]
<watermind>
I get this is because ocaml is strict rather than lazy (as e.g. haskell)
<watermind>
but I was still wondering, is this always preferable in every circumstance to the "usual" fold_right implementation in lazy languages
<watermind>
i.e. where the non-base case is given by fold_right (x::xs) ~f ~init = f y (fold_right xs ~f ~init)
<watermind>
or are there some cases where the latter would be preferable even in ocaml?
<Anarchos>
watermind i never had to tweak the code for perf with ocaml :)
<Anarchos>
good night watermind
Anarchos has quit [Quit: need to sleep]
watermind has quit [Quit: Konversation terminated!]
ben_zen has joined #ocaml
zarus has joined #ocaml
csakatoku has joined #ocaml
lusory has joined #ocaml
breakds has joined #ocaml
madroach has quit [Ping timeout: 264 seconds]
madroach has joined #ocaml
watermind has joined #ocaml
<watermind>
I was trying to report a bug to an ocaml package but things didn't go that well
<watermind>
how can I close an issue that I myself opened
<watermind>
?
<watermind>
EDIT only allows me to edit it, not remove it
watermind has quit [Quit: Konversation terminated!]
walter has joined #ocaml
walter has quit [Client Quit]
mfp has quit [Ping timeout: 246 seconds]
ollehar has joined #ocaml
tobiasBora has quit [Quit: Konversation terminated!]
zarus has quit [Ping timeout: 248 seconds]
Neros has quit [Ping timeout: 248 seconds]
ygrek has joined #ocaml
ygrek has quit [Ping timeout: 264 seconds]
q66 has quit [Quit: Leaving]
ollehar has quit [Ping timeout: 256 seconds]
manud has quit [Ping timeout: 256 seconds]
ygrek has joined #ocaml
Drup has quit [Quit: Leaving.]
darkf has joined #ocaml
shinnya has quit [Ping timeout: 245 seconds]
breakds has quit [Quit: Konversation terminated!]
yacks has joined #ocaml
pr has quit [Ping timeout: 260 seconds]
pr has joined #ocaml
arquebus has joined #ocaml
<technomancy>
so sprintf does funny things with arity it seems
<technomancy>
if I give it a variable in the first position instead of a literal string it gets very confused about arity
<technomancy>
which kinda makes sense, but is there a way to hint it?
arquebus has quit [Quit: Konversation terminated!]
<whitequark>
you have to give a literal string
<technomancy>
is there a name for that kind of special case?
<technomancy>
it's weird to see restrictions like that where normal evaluation rules don't apply
<technomancy>
it must be some kind of macro-like thing, I guess?
yacks has quit [Quit: Leaving]
troydm has quit [Ping timeout: 264 seconds]
<whitequark>
technomancy: it's a hack in the type system: if the inferencer looks at a literal string and it's used in a context where a format string is expected
<whitequark>
it transforms it into that weird format6 thingy
<whitequark>
totally special-cased.
<technomancy>
gotcha; thanks
talzeus has joined #ocaml
talzeus_ has quit [Ping timeout: 268 seconds]
asmanur_ has joined #ocaml
asmanur has quit [Ping timeout: 276 seconds]
<whitequark>
wow, I broke ocaml
<whitequark>
it segfaulted.
<whitequark>
no, I'm not using Obj
<whitequark>
nevermind, I'm using a C library and it's the problem
<skd>
thanks a lot companion_cube, I will have a read through it
mcclurmc has joined #ocaml
<gasche>
companion_cube: if someone wants to do strong verification on ML-style program, and they don't mind experimental/non-maintained, another possibility is CFML, the result of Arthur Chargueraud's thesis
<gasche>
it takes OCaml programs and produces a "characteristic formula" in Coq that has an equivalent semantics
<companion_cube>
gasche: I'm no expert on this, I just happen to know people of the why team ^^
<kerneis>
I should definitely read the doc, I'm using only omnicompletion right now
<kerneis>
but it is still extremely useful
<gasche>
it's actually good practice to explicit close the sentence just before the "free experimentation area"
<gasche>
(I mean use ;;)
<gasche>
because otherwise the parser has all changes to get it wrong
<gasche>
*chances
<rks`>
kerneis: thank you :)
<def-lkb>
gasche: so many people did this mistake that I relaxed the typer in the experimental version to process "open …" asap, even if there is syntax error just after
<def-lkb>
s/typer/parser/
<gasche>
I saw the bug report
<gasche>
but I understand you special-cased `open`, while it may happen with other constructs
Yoric has quit [Ping timeout: 246 seconds]
<def-lkb>
non, it applies to all constructs "top-level" constructs
<gasche>
def-lkb: I think it should be possible to play with the parser to use only the shortest valid prefix, instead of imposing an EOF at the end
<def-lkb>
gasche: the EOF is generated by outline_parser
<def-lkb>
So it's not end-of-file but end-of-definition
<gasche>
yep
<gasche>
but for the last outline
<gasche>
you may want to allow parsing only a valid prefix of the input
<gasche>
and accept that
<gasche>
hm
<gasche>
it may be what you already do, I'm not familiar with what the parser does
<gasche>
but I had the impression that would solve the 'open' problem we're discussing
ollehar has joined #ocaml
<gasche>
(I'm a fan of the ProofGeneral-like "blue zone of safety and calm"; this visual hint makes not-parsing-until-the-end acceptable as the user has feedback on where it stopped)
<def-lkb>
any error after a valid prefix cause the generation of a new "chunk"
<gasche>
I was more suggesting to remove the EOF before top_structure (or rather to retry without it)
<gasche>
I'm not sure whether the two proposals are equivalent
<Kakadu>
well, I definitely need to find some time to test merlin
<def-lkb>
EOF before top_structure ?
<def-lkb>
Kakadu: sure, you have to :)
<Kakadu>
it seems I even have fresh debian virtualbox nearby
<Kakadu>
does merlin writes all what is needed to vim/emacs config after installation?
<gasche>
def-lkb: after top_structure
<gasche>
I mean the starting nonterminal of your grammar forces an EOF at the end of the stream
<gasche>
so you have to go all the way, and possible consume some of the end in an "error" token
<gasche>
without the EOF, the parser would actually stop at the shortest valid prefix
<rks`>
Kakadu: what do you mean?
<gasche>
I'm not sure the two behaviors are identical
<gasche>
(possible error gives you the longest valid prefix, which is a better choice I suppose)
<def-lkb>
gasche: ah, I see… this parser works by side-effects, emit_top raise an exception
<Kakadu>
rks`: I mean that I want to run `opam install merlin`. After that I want to say 'yes' in a question `Do you want to add merlin's config lines to your .vimrc?` and after that I want to have vim with merlin, with completion, where anything works. Out-of-box I mean
<rks`>
yes well, that won't happen, sorry
<rks`>
you need to had two lines to your vimrc
<rks`>
opam doesn't offer what you're asking for (for the moment at least)
Yoric has joined #ocaml
<Kakadu>
Really doesn't?
ocp has joined #ocaml
<rks`>
not that I know of at least
<rks`>
maybe thomasga will prove me wrong.
<Kakadu>
Why you can't write this 'installation script' and add its executeion as last build step?
<def-lkb>
Kakadu: because opam filter output
<Kakadu>
aah
<def-lkb>
It seems that v1.1 adds this possibility
<rks`>
well, it adds the possibility to print things
<Kakadu>
okay, I understood
<rks`>
but I didn't hear anything about asking questions to the user.
<Kakadu>
rks`: opam asks :)
<rks`>
:)
<thomasga>
you can 'opam install merlin —verbose'
<thomasga>
if you want to see the script output
<rks`>
oh, that's nice
<thomasga>
but otherwise yup, that will just be stuck
<thomasga>
(waiting for user input I mean, but without telling him so)
<thomasga>
I guess that's not a very good user interface :-)
Yoric has quit [Ping timeout: 246 seconds]
<Kakadu>
def-lkb: In merlin's README you use $SHARE_DIR variable which was introduced before. It can confuse vim-newbie (like me). Probably you can tell that 'it usually points to ~/.opam/<ocaml_version>/share or /usr/bin/share' or something like that. Also it is not obvious either I should replave this veriable by my path when adding these 2 line into .vimrc or I can create environment variable in bash and add these tow lines after that without any changes
<kerneis>
Kakadu: there is a bug report with a fix about this already
Elentari has joined #ocaml
<def-lkb>
Kakadu: I know, this is confusing sorry. I have to fix that. kerneis opened a pull request, I did not had time to take a look. Sorry
<def-lkb>
we did not write a working vim is needed, but it is implied by any vim plugin
<kerneis>
I love this
<watermind>
I'm trying to install coq + why3, and considering jumping out of my window
mrpantoufle has joined #ocaml
<rks`>
kerneis: you're saving us from depression :)
<def-lkb>
(a monitor and physical keyboard are highly recommended, though a virtual keyboard may be used)
<watermind>
1 - opam fails when installing coq, due to not knowing some patch level whatever that means, so no opam help
<watermind>
2 - I can compile coq by hand but it doesn't find ocamlp5 and uses ocamlp4
<watermind>
3 - when installing why3 it complains about Reference to undefined global `Camlp4'. in coq's file grammar.cma.
<watermind>
^ so that's where I stand
<Kakadu>
'opam install coq --debug' can give more information
<watermind>
Kakadu: thanks
<Kakadu>
ah, it seems you already did it
<watermind>
well I did manage to install it by hand
<watermind>
but not with opam
<watermind>
wait
<watermind>
eh, I think I know
<thomasga>
(—verbose instead of —debug for this kind of issues)
<watermind>
Kakadu: I think that may have fixed it... I didn't have the patch utility. With verbose it became clear it was running some patch command I did not have
<watermind>
Kakadu: with "debug" I mean
<watermind>
thomasga: yes I didn't know that
<Kakadu>
so `which patch` returns nothing?
<watermind>
and opam install now is using camlp5 by specifing its dir with the approapriate flag so that is working
<watermind>
Kakadu: I already installed patch now, it's working
<gasche>
watermind: I wanted to mention that you may be interested in http://www.chargueraud.org/softs/cfml/ as well (a tool to help write correct functional programs)
<gasche>
if you install end-user programs through OPAM, such as Coq, Why3 or Frama-C, be sure to install them in a separate switch from your usual "ocaml development environment" setup
<gasche>
otherwise at some point a library change to you dev setup will rebuild coq, and you *really* don't want that to happen
<Kakadu>
pippijn: don't think that they so unreadable are
<Kakadu>
They are just Coq
<Kakadu>
maybe they aren't only after reading a couple of parts Pierce's book
q66 has joined #ocaml
ygrek has joined #ocaml
ygrek has quit [Ping timeout: 264 seconds]
<watermind>
gasche: oh thank you, yes it looks pretty cool
<watermind>
gasche: hmmm I see what you mean regarding separation, makes sense, got to see how to do that
ocp has quit [Ping timeout: 264 seconds]
<watermind>
gasche: it does confuse me a bit though, in the sense that because there is a dependency between some of them (e.g. why3 requires coq) I still want why3 to pull whatever coq version it needs
<watermind>
since why3 is really what I was trying to install
<pippijn>
what are you doing with why?
<watermind>
pippijn: indirectly, I want to use frama-c which uses why. But I also want to see how much I can do with why in terms of development of correct ocaml programs
<gasche>
watermind: I'm not saying that each program should go to its own switch
<pippijn>
ok
<pippijn>
what are you doing with frama-c?
<watermind>
gasche: to be honest I still have no idea how this "keeping packages" separate works, and what are switches and what not... therefore me being a bit lost
<gasche>
pippijn: re. coq proofs, they are meant to be understood when replaying them interactively, which is why "dry" reading often doesn't offer much insight
<gasche>
watermind: OPAM can manage several separate installations of "ocaml plus stuff"
<gasche>
those are called "switches"
<watermind>
pippijn: frama-c I'm using mostly for acsl, a C specification language, to prove correctness of programs
<pippijn>
watermind: which plugin?
<gasche>
they're useful to experiment with different ocaml versions (eg. have a switch with 3.12.1 and one with 4.00.1, with essentially the same packaged in both cases)
<pippijn>
jessie?
<watermind>
gasche: I see, and each switch is kept consistent amongst itself right?
<gasche>
yes
<watermind>
pippijn: I was with jessie before now I wanted to try wp
<pippijn>
ok
<pippijn>
do you do things with dynamic memory allocation?
<gasche>
or also to experiment with several different environments (eg. you want to experiment with two versions of the same library, and they cannot live in the same switch)
<watermind>
gasche: that seems rather useful, but it will require quite a bit of duplication no?
<gasche>
yes, any package available on both switches will be duplicated
<gasche>
in practice it's probably not that much
<watermind>
pippijn: I haven't done much with it yet, but yes I want to play around with memory allocation
<pippijn>
ok
<pippijn>
because I remember running into some problems with that
<watermind>
gasche: yeap it does sound worth it, I should do that
<gasche>
my "dev environment" switch has packages for, say, JSON, networking, data-structures, etc., Coq/Why3/Frama-C won't need any of that
<gasche>
in practice I don't have a separate "coq-stuff" switch, because for that I use Debian packages
<gasche>
I assume you live in a hostile environment that doesn't have packages for these tools
<watermind>
gasche: yeap to be honest so far my environment is mostly jane street's core plus this specification stuff
<watermind>
this is just something I'm doing on the side, got way too much work in my hands now
<gasche>
(I found little advantage in using a source-based package manager to handle my end-user programs; my operating system packager does that just fine)
<gasche>
(but Coq experts that want to try several versions in parallel and all can have a use for switches as well)
<watermind>
makes sense, but I'm using opensuse and an old version at that
n06rin has quit [Read error: Connection reset by peer]
<mrvn>
gasche: I have chroots or stow for that
<watermind>
not that easy to find packages
<watermind>
much less consistent ones
<watermind>
regarding why3 and whyML I was just a bit disappointed that even though why is written in ocaml, and whyML an ML like language, there is still no specification system for OCaml
<watermind>
in the sense that there is for C with frama-c acsl, or for Ada with the gnat tools
<pippijn>
yes, I would like to have such a thing
<pippijn>
I quite like acsl
<watermind>
indeed
<watermind>
it's cool to extract ocaml from whyml, but if I want to focus on the program and then prove whatever I can that is not a great approach
<gasche>
watermind: there is a prototype of an extension of OCaml with contracts if you're interested
<gasche>
the prototype I was thinking of is the previous work "Dynamic contract checking for OCaml", but this seems a bit more advanced
<watermind>
interesting
<gasche>
that said, none of the tools we mentioned will allow you to add static strong correctness guarantees to existing (unrestricted) OCaml programs after the fact
<gasche>
doing something like that for languages as large as current functional languages has simply never been pulled off outside of research prototypes restricting the problem space (language subset, specification subset, etc.)
<watermind>
right, this really is an extension to ocaml
<gasche>
two Haskell teams are working on realistic static contract verification using SAT-solving
<gasche>
they may get something working for the whole language in a reasonable timeframe
<watermind>
I like the acsl approach where you have C and then specifications in comments,
<watermind>
gasche: yes I've looked at some of the work in haskell
<gasche>
but right now if you want to write programs with strong correctness properties, writing them directly in Coq is probably your best bet
<gasche>
Why3 is nice, but it's limited on the functional end
<watermind>
right...
<gasche>
there was some work to merge the imperative features of Why3 with the higher-order features of Pangolin, but it never left the prototype stage because there is not enough manpower on this
<watermind>
never heard of pangolin, got to look at it too
<gasche>
Pangolin is the PhD thesis of Yann Régis-Gianas, a nice design for higher-order Hoare logic for a pure subset of ML
<gasche>
there was some work with Johannes Kanig that led to "Who", a merge of Why's verification tools with Pangolin's language features, but the Why team concentrates on the imperative features for now
<watermind>
it's somewhat odd that we're more advanced in proving properties of stateful imperative programs that even pure functional programs
<gasche>
(on the other hand, implementing verified software directly in Coq has been proved practical on a large scale by Compcert, the C compiler)
walter has quit [Read error: Connection reset by peer]
<gasche>
watermind: in a large part that's where the money is
<watermind>
true
<watermind>
brb
<gasche>
in the US in particular there is much more funding for verification works on Java programs, and propositional logic (SAT solvers etc.) than functional programs and higher-order logics
walter has joined #ocaml
<gasche>
(with the Microsoft people dedicating a lot of talent and energy to first-order solutions and tools for .NET languages)
ocp has joined #ocaml
<companion_cube>
also, higher-order logic is *hard*
<mrvn>
companion_cube: you must be high to understand it
<companion_cube>
:)
<gasche>
well the amount of effort invested in higher-order logic is nothing compared to the one put in SAT or SMT solvers
<companion_cube>
the complexity class are not the same either
<companion_cube>
NP-complete vs undecidable
<gasche>
we'd probably be in a much better position, had the automated theorem proving community dedicated 10% of its time to higher-order logic
<companion_cube>
it's getting better, though
<gasche>
companion_cube: that wouldn't make much of a difference if the ways to evaluate algorithms is to run them again a pit of problems until a given timeout
<companion_cube>
there are several provers now!
<gasche>
in practice SMT solvers don't terminate on the instances they find too hard
<gasche>
pippijn: did you see the Bison 3.0 release?
<companion_cube>
right, but that still has a big influence on the algorith,s
<companion_cube>
algorithms
<gasche>
(I'm just saying that you may be interested in the changelog, which is not all that fantastic however; but it's not as dead as some other base tools)
<pippijn>
gasche: I'm reading it now, thanks
<pippijn>
I'm always interested
<pippijn>
funny
<pippijn>
they copied gcc's diagnostics
<pippijn>
bison: warnings being treated as errors
<pippijn>
etc.
<ggole>
Might be a library
breakds has quit [Quit: Konversation terminated!]
ollehar has quit [Ping timeout: 276 seconds]
<pippijn>
I like the semantic predicate thing
<pippijn>
I have that in my GLR parser generator
<gasche>
that's precisely like "when" in OCaml pattern-matching
<pippijn>
yes
<gasche>
(a feature that is easy to abuse but still sometimes convenient)
<pippijn>
it's not strictly necessary
<pippijn>
it's just an optimisation
<pippijn>
you can always have the full parse graph and prune it later
<pippijn>
but if you already know it while parsing, you can drop edges right away
<pippijn>
gasche: ok, besides the predicates, there is nothing really great in there
<pippijn>
but it's nice
<pippijn>
they do things
<companion_cube>
"when" is so important..
<companion_cube>
gasche: btw, a prover (satallax) for higher-order logic uses a SAT-solver extensively
<companion_cube>
SAT solvers are very useful even outside of purely propositional logic
<mrvn>
Anickyan: for example for render html
<mrvn>
companion_cube: ^
<pippijn>
and for linux package systems
<pippijn>
there is some distribution that uses a SAT solver for its dependencies
ocp has quit [Ping timeout: 256 seconds]
<mrvn>
pippijn: and why not. with all the work poured into SATs they work well.
<pippijn>
right
<watermind>
companion_cube: gasche: I'm guessing most common higher order programs live in reasonably well behaved restriction where much could still be done though even in the presence of theoretical undecidability
<companion_cube>
I'm not sure, HO contains a lot of sources of undecidability :)
<companion_cube>
it's so undecidable that even *unification* is undecidable
<mrvn>
unless you limit the type system, which most do.
<companion_cube>
but we have to be careful not to make confusion between higher order *logic* (used to express properties of the program) and higher order *types* that are used in ML
<watermind>
exactly I was going to ask that, does the use of HO functions really imply you must move to HO logic to express assertions
<watermind>
it's not obvious to me that we do
<companion_cube>
you can encode some subset of it in first-order logic
<companion_cube>
but you won't be able to reason modulo beta-reduction, for instance
<watermind>
companion_cube: do you know of some source where I could read about that? I'm missing quite a bit of intuition
<companion_cube>
hmmmm :/
<watermind>
no worries if you don't
<companion_cube>
maybe some papers on "who", the tool gasche referred to
<companion_cube>
HO theorem proving is also a very interesting field
<pippijn>
who, why, what
<watermind>
indeed they need to start thinking of better names, this is a nightmare search online
<companion_cube>
:)
<watermind>
I suspect the whole idea is to make us memorise the name of the authors, which is the easiest way to find the tools
<companion_cube>
hmmm
<companion_cube>
look for Johannes Kanig, Jena-Christophe Filliatr
<companion_cube>
+e
<watermind>
yeap I got it already
<watermind>
thanks
zpe_ has joined #ocaml
zpe has quit [Read error: Connection reset by peer]
<jpdeplaix>
I feel like nobody told Gerd that ocamlnet doesn't compiles with ocaml 4.01 :/
zpe_ has quit [Read error: Connection reset by peer]
zpe has joined #ocaml
<gasche>
jpdeplaix: you could send a mail to ocamlnet-devel
<mrvn>
and a patch
<gasche>
the patch is already in OPAM
<gasche>
(though that may be a tactless way to present it)
<gasche>
yeah, you could probably attach the two-lines patch directly to your email
<jpdeplaix>
gasche: are you sure ? Because it still fail to compile :/
<jpdeplaix>
the patches are not related to CLOEXEC
<jpdeplaix>
but yes I can send an email
smondet has quit [Remote host closed the connection]
ygrek has joined #ocaml
smondet has joined #ocaml
<Kakadu>
I've heard that in OCaml pattern matching over strings is ineffective. What about pattern-matching over chars? Maybe there some other cases of pattern matching which are ineffective too?
<ggole>
'ineffective'?
<Kakadu>
yep
<Kakadu>
I think it allocates to many string while pattern matching over them>
<Kakadu>
?
<Kakadu>
too*
<Kakadu>
too many strings*
<ggole>
Hmm
<companion_cube>
why would it allocate?
<ggole>
I've never investigated it
<ggole>
Of course absolutely everything allocates in OCaml...
<ggole>
But not necessarily a lot
<companion_cube>
not really...
<mrvn>
Kakadu: what do you mean? match s with _ when s = "foo" -> | _ when s = "bla" -> ...?
<ggole>
Even array accesses allocate (conditionally)
<companion_cube>
ggole: if they raise an exception, you mean
<companion_cube>
but it's an exceptional situation :P
<ggole>
No
<ggole>
Well, yes. But also if they are a float.
<companion_cube>
a float?
<def-lkb>
right
<companion_cube>
ah, right
<companion_cube>
because you need to unbox
<companion_cube>
but string comparison shouldn't allocate
<def-lkb>
Kakadu: I may be wrong, but pattern matching does no allocation
<mrvn>
ggole: floats are boxed but floats in arrays are not. So when extracting them they get boxed.
<ggole>
I'm seeing allocation in test code, but afaict it's just to handle errors.
<def-lkb>
the string literal to compare to has to be "allocated", but only once in the module, not on every matching
ollehar has joined #ocaml
<ggole>
mrvn: yes, it's the price of universal representation. :(
<companion_cube>
mrvn: they may be boxed in arrays, for instance in case of polymorphism, I think
<ggole>
If they are boxed in the array, you don't have to allocate another one.
<companion_cube>
indeed
<mrvn>
companion_cube: but then access shouldn't allocate
<ggole>
Er, or maybe you do: to avoid somebody stomping on your float.
<ggole>
The semantics are copying, after all.
<ggole>
Hmm.
<ggole>
I'm seeing pretty poor code, but no allocation.
<mrvn>
ggole: f +. 1.0 will allocate
<companion_cube>
ggole: I don't think so, floats are immutable
<ggole>
But arrays are not immutable? And in a float-specialised array, the storage is in line.
<ggole>
(If you were referring to polymorphic arrays, then never mind.)
<mrvn>
ggole: which is why they get boxed on access
<ggole>
Hmm, I would expect a binary search or some more refined scheme. But it just calls caml_string_notequal once for each case.
<ggole>
mrvn: yeah :(
<ggole>
(And as you point out, polymorphic array accesses don't allocate.)
<mrvn>
ggole: what code construct are you talking about?
<ggole>
Matching on strings.
<ggole>
Zero allocation though.
<ggole>
It seems fixable, just probably hasn't got any attention.
<mrvn>
ggole: so "match s with "hallo" -> ()"?
<ggole>
Yes, but with many cases.
<mrvn>
ggole: same applies to match x with Foo -> () | Bar -> () | Baz -> ()
<jpdeplaix>
gasche: sent !
<ggole>
I think codegen for variants is pretty good. I've checked.
<mrvn>
ggole: does it build a binary search tree?
<companion_cube>
ggole: for small pattern matching expressions it probably pays to keep the naive implementation
<ggole>
You can actually do "ternary" search
<mrvn>
ggole: right. <, =, >
<ggole>
By something like cmp value, K/jg L1/je l2/ and then fallthrough to the next case.
<ggole>
And OCaml does this.
<companion_cube>
that is quite good then
<ggole>
And for larger numbers of legs, it will construct a jump table.
<mrvn>
ggole: does it do that for match x with 1 | 2 | 3 | 4 | ... too?
<ggole>
Not sure.
csakatoku has joined #ocaml
<mrvn>
ggole: because that would be nearly the same as string compare
<ggole>
Seems to do ok with ints.
<ggole>
That's with contiguous ranges: lemme try with random ints
<ggole>
One comparison each for this test. Hmm.
<ggole>
There doesn't seem to be a binary search strategy.
<ggole>
Oh no, there is. Never mind.
<ggole>
This output is just hard to read with all the cfi junk.
chambart has joined #ocaml
<companion_cube>
ggole: which output are you reading?
<gasche>
-dlambda is what would make sense, but it doesn't have cfi
<gasche>
-dcmm is the next best bet (and it probably still doesn't have cfi?)
<thomasga>
cfi are inserted in the generated assembly file
<thomasga>
so you'll see them with -S only
<companion_cube>
gasche: to implement Hindley-Milner, I guess I need to represent type quantifiers explicitely?
<gasche>
you don't need to
<gasche>
you can just track levels
<companion_cube>
so, when should I rename variables?
<ggole>
I'm looking at -S indeed.
<gasche>
companion_cube: if you want an implementation that is simple, go read Jean-Cristophe Filliatre's compilation lecture notes
<companion_cube>
hmmmm, right
<gasche>
if you want an implementation that is really efficient, go read Oleg's article on level-handling
<thomasga>
Oleg article is nice indeed
<gasche>
(something about similarities between type inference and region typing)
<companion_cube>
awww, I need something simple at first
<thomasga>
well the result is simple
<rks`>
oleg article is really readable
<rks`>
+'s
<thomasga>
the explanation on why it's working is a bit more complex
<rks`>
s/readable/accessible
<thomasga>
but yea, the article is accessible
<ggole>
Can't you use disjoint sets for unification? Those are very easy to implement.
<companion_cube>
unification is the easy part
<ggole>
I must have forgotten most of what I know about HM. What's the hard part?
<companion_cube>
how to manage free/bound variables? :D
dfan has joined #ocaml
<ggole>
Hmm... I had a toy implementation, and I recall that being pretty simple.
<pippijn>
my toy implementation is also very simple
<ggole>
You mean calculating free variable sets in let-expressions to give you type schemas, right?
<pippijn>
what did you write it in?
<ggole>
OCaml
<ggole>
I think I have it sitting around somewhere
<ggole>
(I imagine the code is terrible, since I would have just learned it then.)
<companion_cube>
ggole: what do you call "disjoint set" in this context?
<companion_cube>
some union-find-like structure?
<ggole>
Looks like I count type variables, and remember the count at entry to a let binding expression. Any variable less than that count should not be generalised.
<ggole>
Yes, union-find.
<companion_cube>
hmmmm, maybe I shouldn't use purely functional structures ^^
<ggole>
It's useful for equating sets of type variables.
n06rin has quit [Read error: Connection reset by peer]
<pippijn>
my hm uses functional data structures
<pippijn>
but it's basically a big fold
<pippijn>
so actually there are always a lot of changes
<companion_cube>
currently I represent substitutions using a Map
n06rin has joined #ocaml
osho0000 has joined #ocaml
<ggole>
Looks like for unioning a type variable and a concrete type, I have an operation to assign the representative of the disjoint set...
<ggole>
Mutable state everywhere. -_-
<ggole>
I bet it is broken.
levi has joined #ocaml
<companion_cube>
the fun part is: I have De Bruijn indexes, free variables, and named symbols
<companion_cube>
yay ^^
osho0000 has quit [Quit: Page closed]
Sim_n has joined #ocaml
hkBst has quit [Quit: Konversation terminated!]
Simn has quit [Read error: Operation timed out]
<watermind>
companion_cube: I keep meaning to try this implementation I had in mind, but for lazy languages
<watermind>
the idea is that you can use the tie the not technique to put labels in your nodes, and these labels act as pointers to some constant reference
Yoric has joined #ocaml
<watermind>
now problem is you can't update the label
<watermind>
but
<watermind>
but instead of making the label some finite character tag or anything of the sort, you make it e.g., an infinite stream
<watermind>
so the tag is defined as you need it
<watermind>
and you need to define it further when you need to make sure the labels in two structures are disjoint
<watermind>
(pretty confusing I know)
weie has quit [Quit: Leaving...]
csakatoku has quit [Remote host closed the connection]
<companion_cube>
I've been starting a library for first-order logic, tired of rewriting always the same stuff
Kakadu has quit [Quit: Konversation terminated!]
csakatoku has joined #ocaml
watermind has quit [Quit: Konversation terminated!]
csakatoku has quit [Ping timeout: 245 seconds]
ygrek has quit [Ping timeout: 256 seconds]
skchrko has quit [Quit: Leaving]
<flux>
could someone just write a type inference module other people would be able to re-use at ease?-)
<companion_cube>
flux: I think it depends too much on the representation of terms and types
eikke has quit [Ping timeout: 264 seconds]
<fds>
I'm playing around with code from this webpage/book http://www.cl.cam.ac.uk/~jrh13/atp/index.html and I'm getting the error "Parse error: unknown directive #install_printer". Can anyone help? It might be something to do with having OCaml 3.21 and 4.0 installed side by side?
<fds>
3.12, sorry.
<companion_cube>
it only works in the toplevel, just to be sure
<fds>
Oh, I see.
<kerneis>
another merlin question:
<kerneis>
is it expected that :Locate works only inside the current file (ie. doesn't jump to a definition in another file, failing with "not found")?
<ggole>
fds: .ocamlinit is useful for that kind of thing
<kerneis>
rks` def-lkb ^
<fds>
ggole: Thanks, but I think what I want is an executable which will take me to top-level where I can type logical formulae (and it will tell me whether or not they're satisfiable), rather than use the OCaml top-level itself.
void64 has joined #ocaml
csakatoku has joined #ocaml
void64 has quit [Read error: Connection reset by peer]
csakatoku has quit [Ping timeout: 240 seconds]
ontologi1e has quit [Read error: Operation timed out]
ontologiae has quit [Ping timeout: 264 seconds]
ollehar has quit [Ping timeout: 264 seconds]
Neros has quit [Ping timeout: 245 seconds]
Elentari has quit [Ping timeout: 250 seconds]
n06rin has quit [Read error: Connection reset by peer]
ulfdoz has joined #ocaml
n06rin has joined #ocaml
n06rin has left #ocaml []
zpe has quit [Remote host closed the connection]
tobiasBora has quit [Quit: Konversation terminated!]
tobiasBora has joined #ocaml
lopex has quit [Ping timeout: 260 seconds]
lopex has joined #ocaml
chambart has quit [Ping timeout: 245 seconds]
tobiasBora has quit [Quit: Konversation terminated!]
mcclurmc has quit [Quit: Leaving.]
yezariaely has joined #ocaml
eikke has joined #ocaml
zpe has joined #ocaml
Neros has joined #ocaml
mfp has quit [Ping timeout: 256 seconds]
mfp has joined #ocaml
ocp has joined #ocaml
Yoric has joined #ocaml
beginner42 has joined #ocaml
<beginner42>
dsheets: did the git repo work for you?
Yoric has quit [Ping timeout: 246 seconds]
<flux>
companion_cube, but with functors?
osa1 has joined #ocaml
<companion_cube>
flux: even with functors, you cannot parametrize on types and still be able to pattern-match
<thomasga>
any idea how to tell oasis to compile a mli without any corresponding ml ?
<watermind>
so I've added why.el to my emacs site-lisp, but still got no why mode on emacs :-/
<watermind>
eh nevermind
<watermind>
syntax mistakes
Yoric has quit [Ping timeout: 246 seconds]
<watermind>
it really messes with my mind that why3 borrows from the syntax of both OCaml and Haskell
<watermind>
and to an extent, same with Agda
csakatoku has joined #ocaml
ocp1 has quit [Quit: Leaving.]
ocp has joined #ocaml
Yoric has joined #ocaml
csakatoku has quit [Ping timeout: 264 seconds]
ocp has quit [Ping timeout: 246 seconds]
eikke has quit [Ping timeout: 276 seconds]
osa1 has quit [Quit: Konversation terminated!]
Yoric has quit [Ping timeout: 246 seconds]
_andre has quit [Quit: leaving]
Anarchos has joined #ocaml
<Anarchos>
say i have a list, what is the best way to remove duplicates in it ?
<companion_cube>
I'd turn it into a set :)
walter has joined #ocaml
csakatoku has joined #ocaml
<Anarchos>
companion_cube sure, but in fact it is only the first components on an assoc list that i want to filter on...
<companion_cube>
well, assoc will take the first matching result
<Anarchos>
companion_cube i need to take the assoc only if there is only one occurence of the key.
demonimin has quit [Ping timeout: 246 seconds]
<companion_cube>
awww
demonimin has joined #ocaml
eikke has joined #ocaml
csakatoku has quit [Ping timeout: 256 seconds]
<whitequark>
Anarchos: maybe fold it with a set of keys as accumulator?
Snark has quit [Quit: leaving]
<Anarchos>
whitequark i know how to do it, i am just looking for the good way to do it
<whitequark>
define "good"
Yoric has joined #ocaml
<Anarchos>
whitequark efficient ?
<whitequark>
there's space and time
<Anarchos>
define space and time ?
* Anarchos
likes recursive relativty jokes :p
<companion_cube>
Anarchos: are you sure you want an association list if efficiency matters?
<whitequark>
uses least amount of RAM / least amount of allocations / least amount of runtime.
<whitequark>
your question is very open-ended, perhaps too much to meaningfully answe
<Anarchos>
whitequark let's go for time :)
<companion_cube>
Anarchos: wouldn't a hashtable or a map be more efficient?
<Anarchos>
companion_cube surely
maurer has joined #ocaml
<maurer>
What's the ocaml way of doing conditional compilation depending on the version of a dependency?
<companion_cube>
maurer: awww :/
<companion_cube>
depends on your build system, I guess
<maurer>
:/
<companion_cube>
oasis seems to be able to do that
<maurer>
It's a pretty big project, I can't switch build systems just for this
<maurer>
I was wondering if ocaml had something like ghc's top-of-file pragma that makes it get preprocessed with cpp or something
<maurer>
(at the top level this project uses autotools, sadly)
zpe has quit [Remote host closed the connection]
Yoric has quit [Ping timeout: 246 seconds]
tac has joined #ocaml
<tac>
Ocaml 4 is the latest, right?
<rks`>
kerneis: you need to have cmt presents in your build directories as well as cmi for locate to work
<rks`>
(to have cmt you need to compile your project with -bin-annot)
<companion_cube>
tac: current 4.00.1, next 4.01
<tac>
hi companion_cube
<tac>
thanks
<companion_cube>
hit
<companion_cube>
hi tac*
Yoric has joined #ocaml
<tac>
I'm considering looking into Ocaml for raspberry pi, just for the heck of it
<tac>
to integerate my RPi with my Haskell IRC bot
Sim_n has quit [Read error: Connection reset by peer]
Yoric has quit [Ping timeout: 246 seconds]
thomasga has quit [Quit: Leaving.]
eikke has quit [Ping timeout: 246 seconds]
walter has quit [Read error: Connection reset by peer]
walter has joined #ocaml
gnuvince has quit [Remote host closed the connection]
gnuvince has joined #ocaml
gnuvince has quit [Changing host]
gnuvince has joined #ocaml
<maurer>
So, is there a good way to do templating in general?
<maurer>
I'm trying to switch between Llvm.TargetData and Llvm.DataLayout depending on llvm revision
<maurer>
Like, I have access to the information of which I want to use when I'm about to use the file, but I don't see any option to do preprocessing or anything...
<dsheets>
beginner42, i think i fixed it
ulfdoz has quit [Ping timeout: 268 seconds]
<beginner42>
dsheets: hi, i just send you a mail thanking you :)
walter has quit [Quit: This computer has gone to sleep]
djcoin has quit [Quit: WeeChat 0.4.0]
<Anarchos>
whitequark i found the right way to do it :)
<dsheets>
steshaw_, yes, js_of_ocaml has several large projects under development in it
<beginner42>
no, the result is still the same...
ollehar has joined #ocaml
<beginner42>
dsheets: i still get this warning
<beginner42>
ocamlfind: [WARNING] You have installed DLLs but the directory /home/florian/.opam/4.00.1/lib/stublibs is not mentioned in ld.conf
<beginner42>
should i add something to the ld.conf files manually?
<dsheets>
i get that warning too and it is fine for your application, i believe. it is because other parties will not be able to use the shared objects you install. However, you are the only consumer of these shared objects (your own lib links them) so it is fine that they are not system-visible
<dsheets>
beginner42, can you link normal C code against libzmq?
<beginner42>
i havent tried that, but give me a few minutes and i will see
<beginner42>
dsheets: do i need mor than
<beginner42>
gcc -lzmq hwserver.c
tac has left #ocaml []
<beginner42>
?
<whitequark>
that feeling when you write a function and then realize that you should have used List.fold_left2
<dsheets>
beginner42, don't think so...
<beginner42>
dsheets: how did you install version 3.3 of zeromq?
<dsheets>
I did what you did and got something that claims to be 3.2.4
<beginner42>
hwserver.c:(.text+0x1b): undefined reference to `zmq_version'
<beginner42>
collect2: ld returned 1 exit status
<beginner42>
locate zmq returns nothing
<dsheets>
beginner42, that would be the problem, then
<dsheets>
did you sudo make install the zeromq3x lib?
<beginner42>
/home/florian/dev/lib/ in this folder is zeromq3-x
<dsheets>
locate may lie if you haven't had updatedb run recently (cron or manual)
<dsheets>
beginner42, did you build and install it?
<beginner42>
i did what was described in the INSTALL file
<beginner42>
now i am trying updatedb
<beginner42>
locate zmq gives me no plenty of locations
<dsheets>
the INSTALL file has a lot of words. I did ./autogen.sh; ./configure; make; sudo make install
<beginner42>
thats what i did
<dsheets>
then i had some libzmq.so.3 in /usr/lib/local
<dsheets>
oops /usr/local/lib i mean
<beginner42>
i have libzmq.a libzmq.la libzmq.so libzmq.so.3 and libzmq.so.3.0.0 in my usr local lib
Saizan has left #ocaml []
<dsheets>
and if you $ gcc -c -o foo.o -lzmq foo.c and then $ ldd foo.o?
<beginner42>
not a dynamic executable
<dsheets>
oops, drop -c and use -o foo rather
<beginner42>
/tmp/ccpF8Der.o: In function `main':
<beginner42>
hwserver.c:(.text+0x1b): undefined reference to `zmq_version'
<beginner42>
collect2: ld returned 1 exit status
<dsheets>
something is wrong with your dynamic library link paths and I'm not sure what... you definitely have run ldconfig? Are you modifying your LD paths somehow else?
<beginner42>
i did sudo ldconfig
<beginner42>
and i have set up ubuntu 12.04 this monday, so basically no changes
<dsheets>
$ sudo ldconfig -v | grep -i zmq
<beginner42>
/sbin/ldconfig.real: Path `/opt/NVIDIA-OptiX-SDK-3.0.0-linux64/lib64' given more than once
<beginner42>
/sbin/ldconfig.real: Path `/opt/NVIDIA-OptiX-SDK-3.0.0-linux64/lib64' given more than once
<beginner42>
/sbin/ldconfig.real: Path `/lib/x86_64-linux-gnu' given more than once
<beginner42>
/sbin/ldconfig.real: Path `/usr/lib/x86_64-linux-gnu' given more than once