<d_bot>
<mbacarella> I wonder if ocaml implementations weren't tested because it's too obscure, or if it's not vulnerable because ocaml devs are strong 💪
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
hsw has quit [Quit: Leaving]
hsw has joined #ocaml
<pgiarrusso>
mbacarella: that list has as many PHP libraries as Rust libraries: 1.
<pgiarrusso>
has anybody seen evidence for "FP makes you a better cryptographer"? I haven't.
waleee has quit [Ping timeout: 240 seconds]
<pgiarrusso>
OTOH, even for "smart" people cognitive biases are strong 😅
<pgiarrusso>
(where the scare quotes are not about the people, but about how useful the concept of "smart" is)
<pgiarrusso>
</ot>
meinside has joined #ocaml
rgrinberg has joined #ocaml
rgrinberg has quit [Client Quit]
rgrinberg has joined #ocaml
gdd1 has quit [Ping timeout: 272 seconds]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
sparogy has quit [Remote host closed the connection]
sparogy has joined #ocaml
gdd1 has joined #ocaml
raskol has joined #ocaml
greenbagels has quit [Ping timeout: 240 seconds]
tomku has quit [Ping timeout: 240 seconds]
tomku has joined #ocaml
greenbagels has joined #ocaml
chrisz has quit [Ping timeout: 260 seconds]
chrisz has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
raskol has quit [Ping timeout: 255 seconds]
xgqt has quit [Ping timeout: 240 seconds]
xgqt has joined #ocaml
misterfi1h has joined #ocaml
wingsorc has quit [Ping timeout: 255 seconds]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
Haudegen has joined #ocaml
misterfi1h has quit [Ping timeout: 260 seconds]
mjs22 has joined #ocaml
mjs22 has quit [Quit: mjs22]
gopiandcode has quit [Read error: Connection reset by peer]
gopiandcode has joined #ocaml
azimut has joined #ocaml
azimut_ has joined #ocaml
azimut has quit [Ping timeout: 268 seconds]
jpds has quit [Ping timeout: 268 seconds]
jpds has joined #ocaml
Tuplanolla has joined #ocaml
amk has quit [Remote host closed the connection]
amk has joined #ocaml
Haudegen has quit [Ping timeout: 268 seconds]
mbuf has joined #ocaml
bartholin has joined #ocaml
<d_bot>
<bannerets> companion_cube: yes, but why is injectivity required? is there a way that could be unsafe if the types are not injective?
<pgiarrusso>
bannerets: type checkers are not complete — I suspect you can write your program without injectivity, but you should implement `cast : ('a, 'b) eq -> 'a -> 'b` (by GADT pattern matching), and then `let f (type a b) (prf : (a M.t, b M.t) eq) (x: a M.t) : b M.t = cast prf x;;`
<pgiarrusso>
not sure in OCaml tho! But that'd work in Coq/Haskell/(Scala?)/...
mro has joined #ocaml
<d_bot>
<bannerets> thanks!
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Ping timeout: 264 seconds]
mro has joined #ocaml
gdd1 has quit [Ping timeout: 255 seconds]
gdd1 has joined #ocaml
GreaseMonkey has quit [Quit: No Ping reply in 180 seconds.]
waleee has joined #ocaml
greaser|q has joined #ocaml
cedric has joined #ocaml
<d_bot>
<pseud> does someone have an article to link to which treats the whole subject of dune, ocaml switches and opam ?
<d_bot>
<pseud>
<d_bot>
<pseud> Specifically:
<d_bot>
<pseud> - how to init a new project
<d_bot>
<pseud> - how to add a dependency, have it fetched and be able to use it within e.g. files in `lib/`/`bin/` in case of a dune project (is adding it to `dune-project` enough ? how is it fetched? as part of `dune-build`? No? Then what?)
<d_bot>
<pseud> - what to version, what to ignore (e.g. add `_opam` to `.gitignore`, it's generated from using `ocaml swich`)
<d_bot>
<pseud> - how OTHERS can clone and setup their dev environment from my existing project.
<d_bot>
<pseud>
<d_bot>
<pseud> I halfway expect deps to be in `dune-project`, the `<project>.opam` file to be generated (maybe `.gitignore`-worthy, even?).
<d_bot>
<pseud>
<d_bot>
<pseud> I am struggling to find this. I really find the dune quickstart guide utterly useless for this exact reason. No attention is given to ecosystem newcomers, no attention is given to how dune and opam interact and/or how switches and dune work.
gentauro has quit [Ping timeout: 240 seconds]
raskol has joined #ocaml
waleee has quit [Ping timeout: 248 seconds]
<companion_cube>
there must be some things on ocaml.org
<companion_cube>
but yeah, probably not enough
<companion_cube>
@pseud your can put your deps in dune-project, and have it generate the opam files indeed
<companion_cube>
.gitignore can contain _build, _opam
gentauro has joined #ocaml
raskol has quit [Ping timeout: 240 seconds]
<d_bot>
<pseud> ^ thanks 🙂
<d_bot>
<pseud>
<d_bot>
<pseud> Hm, so if I clone a project using dune, the `<project>.opam` file is generated, and presumably ready to go.
<d_bot>
<pseud> Otherwise, when I add a new dependency to `dune-project` I must always run `dune build`, have the build fail, then run `opam install . --deps-only` ?
mro has quit [Remote host closed the connection]
mro has joined #ocaml
<companion_cube>
ah, I guess that's a way
<companion_cube>
I commit the opam files, btw
<companion_cube>
(allows for `opam pin --dev` and such)
Cypi_ has quit [Ping timeout: 276 seconds]
<d_bot>
<pseud> Yea, I'm mainly asking because this strikes me as a strange thing - so I'd be thinking there was some other approach that I haven't uncovered 🙂
<d_bot>
<pseud>
<d_bot>
<pseud> What's `opam pin --dev` ? Is that related to lock files/locking dependencies in any way ?
<d_bot>
<pseud>
<d_bot>
<pseud> I found some opam documentation on local switches (what I'm trying to use), that `opam lock .` would generate a lock file and `opam install . --deps-only --locked` would install all deps from the lock-file, hopefully ensuring that dev1 and dev2 end up with the same type of environment.
<d_bot>
<pseud>
<d_bot>
<pseud>
<d_bot>
<pseud> If I had to share a ocaml project with a friend, would I then have to communicate to them which version of ocaml to use for their local switch, then tell them to run `opam install . --deps --locked` (provided there's a lock file, drop `--locked` if not).?
<d_bot>
<pseud> Or is there a single command I can run ?
<companion_cube>
so, `opam pin --dev some_package` will, if the package defines a dev-repo, "pin" the pacakge to its main branch
<companion_cube>
so you get a dev version, really
<companion_cube>
hmm yeah I think your command works
azimut_ has quit [Remote host closed the connection]
azimut has joined #ocaml
<d_bot>
<Drup> @companion_cube / gbury : I'm looking for a library for BDD(T) (in my case, T is a custom finite domain with a total order). In particular, I want rather agressive formula simplification. Do you know of something like that or should we try to build that on top of a BDD library ?
<companion_cube>
hmm there's `mlbdd` I think, which shoudl have decent perf
<companion_cube>
otherwise, idk, I'm not too knowledgeable on BDDs
<d_bot>
<Drup> what, there are some pieces of algorithmics-for-logic you are not expert about ?!
<d_bot>
<Drup> I'm ... outraged 😮
<companion_cube>
:p
<d_bot>
<Drup> you are supposed to be my oracle for these kind of things x)
<companion_cube>
if I were you I'd start by trying to do it on top of mlbdd
<d_bot>
<Drup> (but the fact you recomend mlbdd is already import information)
<companion_cube>
keeping an isomorphism between T and int, or sth
<companion_cube>
yeah I looked at it years ago though
mro has quit [Remote host closed the connection]
<d_bot>
<Drup> Yeah, that was sort of the plan, but it will not incorporate custom axioms though
<zozozo>
I haven't yet looked at bdd, so I don't have anything to suggest, but I trust companion_cube's advice, ^^
<d_bot>
<Drup> you too ! 😮
<companion_cube>
well, we're SAT guys :p
<d_bot>
<Drup> yes, but I want to simplify my formulas, not SAT them ! :d
<companion_cube>
I'm curious, what kind of additional simplifications are you thinking of?
<d_bot>
<Drup> for instance, stuff deduced by transitivity/anti symetry of the total order.
<companion_cube>
hmm, so if you had a path with `x<y` and `y<z`, you'd insert `x<z` in it somehow?
fds has quit [Ping timeout: 240 seconds]
fds has joined #ocaml
<d_bot>
<Drup> that, and/or, if I had x<y, y<z and z<x, I would replace by false 🙂
mro has joined #ocaml
mro has quit [Remote host closed the connection]
sagax has quit [Read error: Connection reset by peer]
gareppa has joined #ocaml
<zozozo>
I'd think that in the general case, such simplifications may need an smt-solver like process for each branch of the bdd ?
<d_bot>
<Drup> I'm always kinda surprised there are so few methods/tools to simplify logic formulas
<d_bot>
<cheeze> i can't seem to get the example to work because dune expects the "root" of the project
rgrinberg has joined #ocaml
<d_bot>
<Drup> Not really: find a smaller formula that is equivalent.
<companion_cube>
"a"
<companion_cube>
that's vague :)
<companion_cube>
you can have basic simplifications like SMT solvers do (e.g . Z3.Expr.simplify [])
bartholin has quit [Quit: Leaving]
<zozozo>
Drup : note that this is quite close to the sat/smt problem: a solver tries to find whether a formula (or a set of formula) can reduce to `true` or `false` (which can be seens as the smallest formulas)
<companion_cube>
a problem with BDD is that if the order is wrong, you get a bigger formula :s
<zozozo>
right, you could also try and find the order that minmizes the size of your bdd
<companion_cube>
sure, but that's costly
<companion_cube>
and the BDD community has worked hard on heuristics for that, I think :)
raskol has joined #ocaml
<d_bot>
<Drup> @companion_cube that's on purpose: I do not want minimality, just best effort
<d_bot>
<Drup> also, there are some aspect that I find pretty commonly in my use cases: eliminate intermediary variables. This could be also described as trying to remove existentially quantified variables.
<companion_cube>
a SMT simplifier will often try to apply a few rules, including "one point rule"
<d_bot>
<pseud> packages can be marked as dev packages (dune: `(foo :dev)`, opam: `"foo" {dev}`). They don't seem to be installed when I call `opam install . --deps-only` (which is OK).
<companion_cube>
`x=t ==> F[x]` becomes `F[t]`
<d_bot>
<pseud> But how do I install them >
<d_bot>
<Drup> yeah, that's not exactly sufficient
<companion_cube>
generally people won't care too much about simplification because it's incomplete, and what matters is the solving that comes afterwards
<d_bot>
<Drup> again, I don't want full blown QE, i just want best effort
<d_bot>
<Drup> yeah, in my case I really care about the formula ....
<companion_cube>
you have an unusual use case and that's why no tool exists :)
<d_bot>
<Drup> 😦
<d_bot>
<Drup> Signature inference is not *that* unusual
<companion_cube>
you mean in OCaml?
<d_bot>
<Drup> in general
<companion_cube>
what do you mean by signature inference then?
<companion_cube>
(I mean, I understand it in the context of a ML language)
<d_bot>
<Drup> signature here as in "type signature": You have objects that are built by composition, you have an algebra of signature. You know how to compute signature based on the signature of the combination of the objects. Infer the signature for the whole thingy
<d_bot>
<Drup> it's just not necessarely really programs per-se
<d_bot>
<Drup> Often, the signature is not that difficult to encode into logic formulas
<companion_cube>
ah but it also means you have an intuitionistic `->` ?
<d_bot>
<Drup> you want to return the signature, not just say if it's valid or not
<d_bot>
<Drup> generally, the algebra is simple enough that you don't
<d_bot>
<Drup> (I rarely encode the whole type system that way)
<d_bot>
<Drup> in any case, it's a tool I have used several time, and every time, I have to reinvent ad-hoc tools that I feel should be much more generic
<companion_cube>
🤷
<d_bot>
<Drup> hence, BDD(T) 😄
<d_bot>
<Drup> maybe I should find a BDD expert and try to invent the thing once and for all
<companion_cube>
not sure why you want BDD and not rewriting, though
<d_bot>
<Drup> it's a good question: I want whatever goes fastest and has unique representation.
<d_bot>
<Drup> egg doesn't solve the same problem at all
<companion_cube>
EGG (the second one) is really cool and comes from the compiler community, too
<d_bot>
<Drup> I don't want saturation, the opposite, in fact
<companion_cube>
well
<companion_cube>
it's congruence closure, but where you can associate a normal form to classes
<d_bot>
<Drup> (I know egg quite well :p)
<d_bot>
<Drup> also .... it's going to be much much much much slower than what I want
<companion_cube>
then you've seen that you can associate to each class, the simpler/most reduced aspect of this class?
<companion_cube>
well no
<companion_cube>
faster than Egg? lol good luck with a BDD
<d_bot>
<Drup> it depends for which task ...
<companion_cube>
CC is O(n log(n)) if you do it well
<companion_cube>
I doubt you'll find faster simplifiers that are not naive
raskol has quit [Ping timeout: 268 seconds]
<d_bot>
<Drup> I can try, but pretty sure egg wouldn't get off the ground for what I want
<companion_cube>
do you have an implem of Egg in OCaml?
<d_bot>
<Drup> no, that would be cool
<d_bot>
<Drup> (I would actually like one for another, completely unreleated project)
<companion_cube>
yeah
<companion_cube>
(what are your performance requirements, that Egg is too slow, btw?)
<companion_cube>
I do have a nice congruence closure, but it needs a bit of work to be full EGG
<d_bot>
<Drup> it's a bit complicated, but let's say I have 5M elements in a tree, and I simplify when I combine the branches
<companion_cube>
ah, right :D
<companion_cube>
how many elements if it's in a DAG, btw?
<companion_cube>
or is it 5M DAGs?
<d_bot>
<Drup> a bit less, but still far too much
<d_bot>
<Drup> also, those are the elements, which each have a signature. Those signatures are "not too big", but it still means millions of simplifications to do every time you go up
<companion_cube>
fun stuff
<companion_cube>
well, a congruence closure will do perfect sharing and caching, so it might be more acceptable
<companion_cube>
(what do you mena by "combining the branches")
<d_bot>
<Drup> I don't think the CC will even fit in memory if I put all the signatures in it
<companion_cube>
perhaps not, depends on your term representation
<companion_cube>
but, not to discourage you, but a BDD is generally a lot heavier
mbuf has quit [Quit: Leaving]
<d_bot>
<Drup> I find that surprising, I would think that a BDD is a fairly compact representation of a formula
<companion_cube>
depends on the variable ordering
<companion_cube>
(by a lot)
spip has joined #ocaml
Haudegen has joined #ocaml
<companion_cube>
why is opam so slow
<companion_cube>
:/
<d_bot>
<darrenldl> update?
<companion_cube>
everything is always slow
<d_bot>
<darrenldl> ~~use container for everything~~
<companion_cube>
clearly opam does a lot of disk IO for every operaton
<companion_cube>
operation*
wingsorc has joined #ocaml
<d_bot>
<darrenldl> thats....interesting
<d_bot>
<darrenldl> well opam also does sandboxed build right? wonder if that requires setting things up and causing some slowdown
<rgrinberg>
companion_cube out of all the wheels you've re-invented, you spared opam
<companion_cube>
I don't have the madness to do that, rgrinberg
<companion_cube>
I reinvent small wheels :)
<d_bot>
<darrenldl> copam
<companion_cube>
rgrinberg: btw `dune build @check -w` sometimes still takes a lot of RAM for me
<companion_cube>
(long running, on repos with a lot of changes)
<rgrinberg>
it always takes a lot of ram for me :)
<rgrinberg>
with this whole memoization business, we somewhat forgot that storing all these tables takes memory
<companion_cube>
right
<rgrinberg>
so it's required to bounce dune from time to time
<companion_cube>
is it realistic for dune to clear up old entries from cache after a while?
<rgrinberg>
very realistic. it would mean implementing a GC essentially though
<companion_cube>
for `dune build -w` I think it'd be reasonable for dune to "restart" itself, in a way: clear everything, re-memoize?
<rgrinberg>
Sure, if you don't suffering a "small" delay when doing this
<companion_cube>
typically it's instances of dune running in a project I'm not even working on at the moment :D
motherfsck has quit [Quit: quit]
gareppa has joined #ocaml
motherfsck has joined #ocaml
<d_bot>
<anmonteiro> At least mirage crypto uses curves derived from F*.
<d_bot>
<anmonteiro>
<d_bot>
<anmonteiro> So the answer is verifiable implementations rather than “strong devs” IMO
<d_bot>
<mbacarella> I get your point though. I've never heard of F*
<d_bot>
<mbacarella> *adds to todo list*
<d_bot>
<mbacarella> I'm actually not very clear on what the ed25519 leak is caused by? it sounds like an ambiguous misuse of the signing protocol rather than an implementation error