<rgr[m]>
Armael: i emailed you. fixing this stuff in IRC is a bit of a pain..
jack5638 has quit [Ping timeout: 276 seconds]
jack5638 has joined #ocaml
cobreadmonster has joined #ocaml
silver has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
<discord2>
<Perry> octachron: I think a lot of the tutorial might need some linguistic tuning. Going through it there's a lot of places where a beginner would get confused. This might be a case where some strategic language and maybe another example (perhaps showing record fields being qualified) would help fix the issue.
FreeBirdLjj has joined #ocaml
<discord2>
<Perry> Is it possible to assign this to me in a Mantis ticket even if I'm not an OCaml developer?
FreeBirdLjj has quit [Ping timeout: 250 seconds]
FreeBirdLjj has joined #ocaml
tane has joined #ocaml
<octachron>
Perry, I fear that Mantis can only assign to people with a developper status. But opening a Mantis ticket should be fine, it is not like there are a lot of race hazards on Mantis tickets
<discord2>
<Perry> BTW, it would be good to get steenuil's fixes to the Makefiles in. I find that when I'm editing the manual I want to rebuild a lot, so speeding up the manual build is very useful.
<octachron>
It looked good when I took a glance, I will review more in detail when I am finished with some code example generator's tweak later this week-end.
Walter[m] has quit [*.net *.split]
loxs[m] has quit [*.net *.split]
ansiwen has quit [*.net *.split]
peddie[m] has quit [*.net *.split]
<discord2>
<loxs> Base.List.for_alli seems to return bool and my compiler complains that I don't do anything with the value... Why is this and how should I handle the situation?
Bluddy[m] has quit [Ping timeout: 246 seconds]
M-martinklepsch has quit [Ping timeout: 240 seconds]
rgr[m] has quit [Ping timeout: 240 seconds]
regnat[m] has quit [Ping timeout: 255 seconds]
mmmmmmmmmmmm[m] has quit [Ping timeout: 255 seconds]
M-jimt has quit [Ping timeout: 255 seconds]
drsmkl[m] has quit [Ping timeout: 255 seconds]
Bozghurt[m] has quit [Ping timeout: 246 seconds]
flux[m] has quit [Ping timeout: 246 seconds]
isaachodes[m] has quit [Ping timeout: 246 seconds]
talyian[m] has quit [Ping timeout: 246 seconds]
pmetzger[m] has quit [Ping timeout: 246 seconds]
neatonk[m] has quit [Ping timeout: 260 seconds]
hcarty[m] has quit [Ping timeout: 260 seconds]
olopierpa[m] has quit [Ping timeout: 250 seconds]
aspiwack[m] has quit [Ping timeout: 256 seconds]
bli[m] has quit [Ping timeout: 256 seconds]
tiksin[m] has quit [Ping timeout: 256 seconds]
dlebrecht[m] has quit [Ping timeout: 246 seconds]
multiocracy[m] has quit [Ping timeout: 246 seconds]
yetanotherion[m] has quit [Ping timeout: 276 seconds]
equalunique[m] has quit [Ping timeout: 276 seconds]
copy` has quit [Ping timeout: 255 seconds]
RouvenAssouly[m] has quit [Ping timeout: 255 seconds]
neiluj has quit [Ping timeout: 255 seconds]
hdurer[m] has quit [Ping timeout: 240 seconds]
remix2000[m] has quit [Ping timeout: 240 seconds]
orbifx[m] has quit [Ping timeout: 250 seconds]
srenatus has quit [Ping timeout: 250 seconds]
Haudegen[m] has quit [Ping timeout: 260 seconds]
caseypme[m] has quit [Ping timeout: 260 seconds]
smondet[m] has quit [Ping timeout: 260 seconds]
spectrumgomas[m] has quit [Ping timeout: 260 seconds]
bglm[m] has quit [Ping timeout: 260 seconds]
sh0t has joined #ocaml
sz0 has quit [Quit: Connection closed for inactivity]
FreeBirdLjj has quit [Remote host closed the connection]
pierpal has quit [Ping timeout: 240 seconds]
kakadu has quit [Remote host closed the connection]
pierpal has joined #ocaml
FreeBirdLjj has joined #ocaml
<discord2>
<Perry> loxs: the compiler is almost always right. What are you doing with the value?
ansiwen has joined #ocaml
<discord2>
<loxs> nothing, but I also don't know what to do with this value
<discord2>
<loxs> it's just a byproduct of printing a list
<discord2>
<loxs> so I ended up doing this, which is a bit ugly let _ = List.for_alli ... in
sh0t has quit [Remote host closed the connection]
sh0t has joined #ocaml
bglm[m] has joined #ocaml
multiocracy[m] has joined #ocaml
neiluj has joined #ocaml
RouvenAssouly[m] has joined #ocaml
rgr[m] has joined #ocaml
spectrumgomas[m] has joined #ocaml
hdurer[m] has joined #ocaml
aspiwack[m] has joined #ocaml
remix2000[m] has joined #ocaml
copy` has joined #ocaml
peddie[m] has joined #ocaml
equalunique[m] has joined #ocaml
drsmkl[m] has joined #ocaml
M-jimt has joined #ocaml
smondet[m] has joined #ocaml
M-martinklepsch has joined #ocaml
srenatus has joined #ocaml
Haudegen[m] has joined #ocaml
tiksin[m] has joined #ocaml
dlebrecht[m] has joined #ocaml
pmetzger[m] has joined #ocaml
talyian[m] has joined #ocaml
isaachodes[m] has joined #ocaml
mmmmmmmmmmmm[m] has joined #ocaml
loxs[m] has joined #ocaml
hcarty[m] has joined #ocaml
olopierpa[m] has joined #ocaml
Walter[m] has joined #ocaml
Bozghurt[m] has joined #ocaml
bli[m] has joined #ocaml
yetanotherion[m] has joined #ocaml
neatonk[m] has joined #ocaml
caseypme[m] has joined #ocaml
regnat[m] has joined #ocaml
Bluddy[m] has joined #ocaml
flux[m] has joined #ocaml
orbifx[m] has joined #ocaml
jnavila has joined #ocaml
<discord2>
<Perry> There are worse ways to indicate that you don't care about a return value.
<discord2>
<Perry> @loxs, you've been mentioning a bunch of trouble with types. I'd suggest, as an exercise, you might want to forgo type inference for a few days. Try explicitly naming the types on your functions etc. for a bit, which you're allowed to do of course. It might give you added intuition about the types. You'll get more of a feel for things like type variables, polymorphism, etc. Just a suggestion.
<discord2>
<loxs> I did that! And it helped 😃
<discord2>
<loxs> Now i have a bit too many records, but it seems to work pretty darn well
<discord2>
<loxs> (Also modules, as otherwise working with records is not fun)
dtornabene has quit [Ping timeout: 240 seconds]
Haudegen has joined #ocaml
argent_smith has quit [Ping timeout: 240 seconds]
<Drup>
loxs: if you just want to operate on all elements of a list, the right function is "iter" (and iteri)
<Drup>
`for_all checks that the given boolean function is true on all the values
spew has joined #ocaml
<discord2>
<loxs> I, see, thanks Drup. But why does for_alli exist at all?
<discord2>
<loxs> ah, I see
<discord2>
<loxs> (didn't notice your second line initially)
<Drup>
(I must say, this mistake is a bit surprising :p)
<discord2>
<loxs> of course, there is a meaningful difference between for_each and for_all, but I presume I accepted it easily by inertia
spew has quit [Remote host closed the connection]
spew has joined #ocaml
ctrlsbstr has joined #ocaml
ctrlsbstr has quit [Client Quit]
hdon has joined #ocaml
hdon has quit [Ping timeout: 260 seconds]
ctrlsbstr has joined #ocaml
Soni has quit [Remote host closed the connection]
ctrlsbstr has quit [Client Quit]
Soni has joined #ocaml
cobreadmonster has quit [Quit: Connection closed for inactivity]
jimmyrcom_ has joined #ocaml
ctrlsbstr has joined #ocaml
jimmyrcom_ has quit [Ping timeout: 265 seconds]
sh0t has quit [Ping timeout: 260 seconds]
spew has quit [Remote host closed the connection]
kleimkuhler has joined #ocaml
<discord2>
<Perry> Hey, I expect the answer is "no", but is there such a thing as an OCaml Quick Reference? As a newcomer I often forget particular bits of syntax. (No, looking at the full grammar isn't useful, it's way too big to run in my head.)
<discord2>
<Perry> This might be another thing for a Doc Jam.
<steenuil>
I think there was a card with the syntax
malina has quit [Quit: Throwing apples of Montserrat]
<companion_cube>
it's probably not part of the API, sadly
<companion_cube>
I can't find it, at least
<companion_cube>
it might be worth opening an issue on Z3's repository, or looking for existing such issues
jimmyrcom_ has quit [Ping timeout: 264 seconds]
kleimkuhler has joined #ocaml
<sh0t>
companion_cube, I saw the module FixedPoint on the the api I thought that might be useful...
<companion_cube>
no, it's for relational algebra
<companion_cube>
it's not really targetted at the same things
<sh0t>
oh I see...
<sh0t>
companion_cube, my end goal is to discharge equalities that involve summations of f(n) for n ranging between k and t ... I thought about implementing this with "recursive" sum, hence the question on stackoverflow. But maybe i am approaching it in the wrong way?
<sh0t>
(equalities or in general assertions involving summations...)
<companion_cube>
for k and ti fixed?
<companion_cube>
-i
<companion_cube>
if they're fixed you'd better generate the expabded sum by yourself
<sh0t>
well they are not fixed ...
<sh0t>
:/
<companion_cube>
it's going to be tough then, I think
<companion_cube>
you want/expect to prove unsat?
<sh0t>
yeah of it's sat to see a countermdodel...
<sh0t>
*counter example
<companion_cube>
I suspect your problem is not actually decidable
<sh0t>
I think you are right if you put multiplication in f(n) it's not in general decidable
<companion_cube>
if you want to prove stuff like `Σ_i t_i ≥ 0` you're going to need induction
<sh0t>
but oh ok
<sh0t>
could I not add an "induction" principle as an axiom
<mrvn>
maybe you can break it down so you proove that both sides of the multiplication are the same in both functions.
<sh0t>
?
<mrvn>
if * is generall undecidable then reduce it to a specific and deciable use pattern
<companion_cube>
induction is going to be second order, you can't write it in SMT
<mrvn>
but no diea about z3 and if that is possible or even helfull
<companion_cube>
honestly this kind of proof is too hard for pure automation
<mrvn>
helpfull
<companion_cube>
hellfull, yes :p
<mrvn>
Manually I would proove it by induction: f(1) == g(1) and if f(n) == g(n) then f(n+1) == g(n+1)
<sh0t>
ok companion_cube i see... thanks mrvn i'll think about it.
<mrvn>
sh0t: I think your example should be UNSATISFIABLE because f(20) is undefined behaviour. could do anything.
<companion_cube>
hum?
<sh0t>
?
<mrvn>
signed integer overflow.
<sh0t>
oh ok well...
<companion_cube>
z3 uses bigints
<sh0t>
20!=2432902008176640000 so yea...
<mrvn>
well, bigints would work
<companion_cube>
sh0t: there might be some new tool that combines induction and z3 soon :-)
<companion_cube>
mrvn: z3 only uses bigints. If you want fixed precision then it's the bitvector API :-)
<sh0t>
ok companion_cube
<mrvn>
What exactly is "(assert (= x (f 10)))" supposed to mean? Are you asking if there is a number "x" that equals "f 10". That seems rather pointless since you can just type in "f 10" and get it.
<mrvn>
Or are you asking if "f 10" halts?
<companion_cube>
in this case you could just compute
<companion_cube>
but you could also `(assert (= (f x) 120))` and expect a model with x=6
<companion_cube>
(or 5?)
<mrvn>
companion_cube: might not finish before the universe burns out and still be computable.
<companion_cube>
mrvn: well it's only semi decidable
<companion_cube>
if you ask for `(= (f x) googleplex)` then you shouldn't expect an answer
<companion_cube>
but, you know, it can still be useful
<mrvn>
companion_cube: but (= x (f googleplex)) could easily say SATISFIABLE.
<mrvn>
and (get-model) would then take really long
<sh0t>
ok what if instead of (assert (= x (f 10)))" I typed (assert (= x (f y)))" but adding more constraints on y..for instance 0<y<9...
<mrvn>
anyway: What's the goal in the stackoverlow question? "f 10" is a constant. Seems rather pointless to use that.
<sh0t>
i know in general it's undecidable....
<sh0t>
the point of the question is a syntactical one...i did not knwo how to encode f (recursive) with the ml api...
<sh0t>
any f would do...the computability issue comes later in general it's undecidable but i might add more constraints and "help" the smt...
mk9 has quit [Ping timeout: 240 seconds]
<mrvn>
does the api have anything with a "rec" in the name?
<sh0t>
it has a FixedPoint module which i thought was the way to go but maybe it's not cause it's targeted to relational algebra I m tryign to read more about it...
<companion_cube>
mrvn: how would it know it's satisfiable?
<companion_cube>
you have to find such a `x` before you answer 'SAT'
<companion_cube>
and it might never terminate
<companion_cube>
e.g. if I ask `(= (fact x) 121)` there is no answer, but it's not that easy to show unsat
<companion_cube>
(you basically have to prove monotonicity by *induction* and show it doesn't work up to 6)
<mrvn>
companion_cube: you know x<=1 is satisfiable and if f(n) is then f(n+1) is too. So everything is. You only need to reason with induction.
<companion_cube>
"only"
<mrvn>
companion_cube: for my example of "f googleplex"
<companion_cube>
mrvn: z3 doesn't know about induction
<companion_cube>
and it's deeply undecidable
<mrvn>
companion_cube: yeah, that the problem
<companion_cube>
so why would z3 answer "SAT" in this case?
<mrvn>
companion_cube: without some fixpoint transformation or build-in recusion it wouldn't.
<companion_cube>
exactly, it's a hard problen
<companion_cube>
problem*
<companion_cube>
otoh you can do some form of unfolding (Kuncak, Sutter, Köksal 2011 — I think) you can find small-ish counter-examples relatively easily
<sh0t>
companion_cube, that is in theory my goal... finding small counter examples..
hdon has quit [Ping timeout: 264 seconds]
Haudegen has quit [Read error: Connection reset by peer]
<companion_cube>
sh0t: mine too :-)
hdon has joined #ocaml
kakadu has quit [Remote host closed the connection]