<atchoum>
How can I fix it ? (especially if you don't want to click that link, the problem is that I cannot build ocamlfind with opam because of an `unbound module TopLoop` error). I run on archlinux + ocaml 4.06.0.
<octachron>
atchoum, you probably need the ocaml-compiler-libs package since it seems that archlinux splits compiler-libs from the compiler package
<atchoum>
Tthank you a lot octachron.
<atchoum>
yes indeed
<atchoum>
I have that error now `Unbound module Topkg_result`
<octachron>
Do you have a reason to use a system switch? Letting opam handles all dependendencies tends to be easier (with opam switch 4.06.0 for opam.1 or opam switch create 4.06.0 for opam.2)
<atchoum>
that's what I want to do
<atchoum>
but my system doesn't let me do it
<atchoum>
so you say I should remove all the ocaml related package of my system and start fresh with opam ?
<atchoum>
ok I'll do it.
<atchoum>
4.06.0 is the recommended compiler to have ?
<octachron>
you don't need to remove your distribution package; just creating a new switch from opam should work fine
<octachron>
4.06 seems stable enough now
<octachron>
(even if there is a 4.06.1 release around the corner)
govg has quit [Ping timeout: 240 seconds]
govg has joined #ocaml
shinnya has joined #ocaml
spip has joined #ocaml
mk9 has quit [Quit: mk9]
<spip>
in the REPL, can we do an 'unopen/close/whatever Foo' after an 'open Foo'?
<def`>
in caml light only :P
<spip>
Damn... And an '#unrequire "foo"'?
<def`>
not even sure what that would mean :)
<zolk3ri>
:o
<def`>
(but I think the main answer to your problem is "no you can't" :P)
<def`>
with a few hacks it should be possible to restore a previous version of the environment
<def`>
a "#push/#pop" primitives.
jnavila has joined #ocaml
shinnya has quit [Ping timeout: 240 seconds]
spew has joined #ocaml
FreeBirdLjj has joined #ocaml
<adrien>
was the issue with very long package remova during upgrades to opam2 beta5 known?
<companion_cube>
def`: funny you mention that, we have #push/#pop at my company :D
<companion_cube>
it's hard to beat man-years of effort in implementing these things
<zozozo>
+1
<zv>
companion_cube: yeah, there's quite a bit to z3 that is pretty much just manual optimization spread out over years
<zv>
especially if you are "lifting" the logic of x86 instructions to some symbolic representation, you need that kind of optimization
<zv>
it would be cool if there was some kindof sat/smt discussion forum
<Drup>
well, there is one, it's called TACAS
<Drup>
:3
<companion_cube>
you mean the SMT workshop? ^^
<companion_cube>
or the SAT conference? or CADE?
<companion_cube>
but I get the point, there should be sth on IRC ;p
<zv>
yeah
<zv>
i hear something like TACAS and I think "singapore" when what i'm looking for is the "kowloon walled city". if you know what i mean.
<Drup>
one thing that always surprised me is the relatively few people interested in writing max-sat/smt solvers
<Drup>
lot's of people seem really super happy to write billions of sat solvers that have the same expressive power and a oh-so-very-slightly different perf behavior
<zv>
I've never heard of a "max-sat" solver
<Drup>
but max-sat/smt is crazy useful for lot's of problems and has, like, 2 usable solvers
<Drup>
well, max-smt has 2
slash^ has quit [Read error: Connection reset by peer]
rostero has quit [Quit: Connection closed for inactivity]
<zv>
Drup: what is the difference between a max-sat and a more familiar sat solver?
Haudegen has quit [Remote host closed the connection]
<Drup>
(arguably, I'm only interested by max-smt, though)
<zv>
Drup: i guess I just can't see how any solver could be "more powerful" than a sat solver
<zv>
i've read donald knuth on satisfiability and that is it and he doesn't really address the problem
<zv>
isn't a 3-sat solver essentially universally powerful?
<zv>
any equation, any number of unknowns can be encoded into a conjunction of sat instances, right?
<zv>
i honestly don't know tho
jao has quit [Ping timeout: 268 seconds]
<zv>
i guess I see a little bit how it could be more expressive
<Drup>
zv: that's for decision problems. Optimization under constraints isn't a decision problem. I don't ask "yes or no", I ask "what's the max ?"
<Drup>
and regardless, the ability to encode one problem into the other doesn't mean you can solve actual instances with the encoding
<Drup>
(case in point: I can encode regex equivalence into ocaml typechecking, but that doesn't run well :D)
<zv>
i see, so encoding this into sat would quickly grow huge, because you would have to essentially solve every combination of clauses upto the total.
bartholin has joined #ocaml
<zv>
e.g a solving 4 clauses quickly turns into 24 sat instances
<zv>
that is cool, thank you Drup
<fds>
zv: If you start ##satisfiability, I'll join. ;-)
* orbifx
smirks the discussion spawned. [one just never knows]
<companion_cube>
apparently z3 does max-smt in terms of normal smt
<companion_cube>
as a theory
<Drup>
companion_cube: that, plus some simplex
<zv>
companion_cube: what is the logic name?
<Drup>
well, simplex + a loop to jump between regions that are not connected
<zv>
Drup: how do you apply simplex to a DPLL or CDCL tree?
<zv>
rather, is there a solver that demonstrates this?
<Drup>
well, z3 :D
<Drup>
I don't understand a single thing about sat/smt solving, so you'll need to read papers :p
jimmyrcom has quit [Ping timeout: 248 seconds]
<zozozo>
zv: from what I know it's not that complicated, except if you want some kind of fancy backtracking
<zozozo>
And even then the complexity is more how to efficiently backtrack the simplex state
spew has joined #ocaml
cbot has joined #ocaml
iitalics has joined #ocaml
pierpa has joined #ocaml
nomicflux has quit [Quit: nomicflux]
dtornabene has joined #ocaml
iitalics has quit [Quit: WeeChat 2.0.1]
jbrown has quit [Quit: Leaving]
spew has quit [Ping timeout: 256 seconds]
<kakadu_>
I recently started looking for approach to convert negative information to positive for algebraic datatypes. Basically, when type t = A|B|C I want to convert (x<>A) && (x<>B) to (x==C)
<kakadu_>
Any well-known papers about something like this?
<thizanne>
kakadu_: that looks very similar to pattern matching exhaustivity check
<kakadu_>
I didn't thought about it in this way, thanks :)
jnavila has quit [Remote host closed the connection]
jimmyrcom has joined #ocaml
<Drup>
you could also just call an smt solver :p
zolk3ri has quit [Quit: Lost terminal]
ocaml697 has joined #ocaml
zolk3ri has joined #ocaml
zolk3ri has quit [Client Quit]
<ocaml697>
How do I create a mutable list ? I can create a list - let foo = ([]:float list) ;; But when I then try and alter the list - foo := 1.0::foo;; I get Error: This expression has type float list but an expression was expected of type 'a ref. Thanks
zolk3ri has joined #ocaml
zolk3ri has quit [Client Quit]
<pierpa>
AFAIK, there's not a built in mutable list data structure. You must write your own.
zolk3ri has joined #ocaml
<pierpa>
or, even better, reconsider your choice about data structures
<companion_cube>
type 'a mutlist = Nil | Cons of {mutable hd: 'a; mutable tl: 'a mutlist}
<pierpa>
no wait, from the example, it looks like you don't want a mutable list, but a mutable reference to a list. Correct?
<pierpa>
if so, then just let foo = ref (...)
ocaml697 has quit [Ping timeout: 260 seconds]
zmt00 has quit [Ping timeout: 240 seconds]
zmt00 has joined #ocaml
jimmyrcom has quit [Ping timeout: 256 seconds]
nullifidian_ has joined #ocaml
zolk3ri has quit [Quit: leaving]
nullifidian has quit [Ping timeout: 240 seconds]
jimmyrcom has joined #ocaml
sillyotter has joined #ocaml
nomicflux has joined #ocaml
sh0t has joined #ocaml
sillyotter has quit [Quit: WeeChat 1.9.1]
jimmyrcom has quit [Ping timeout: 256 seconds]
kakadu_ has quit [Remote host closed the connection]
dtornabene has quit [Quit: Leaving]
jimmyrcom has joined #ocaml
cbot has quit [Ping timeout: 260 seconds]
andreas_ has quit [Quit: Connection closed for inactivity]