companion_cube changed the topic of #ocaml to: Discussions about the OCaml programming language | http://www.ocaml.org | OCaml 4.05.0 release notes: https://caml.inria.fr/pub/distrib/ocaml-4.05/notes/Changes | Try OCaml in your browser: http://try.ocamlpro.com | Public channel logs at http://irclog.whitequark.org/ocaml
jlam__ has joined #ocaml
jlam has quit [Ping timeout: 240 seconds]
jlam_ has quit [Ping timeout: 240 seconds]
peterpp has quit [Ping timeout: 240 seconds]
<darktenaibre> __marioxcc: if you augment Coq's logic with LEM, in terms of equiconsistency, this is essentially ZFC + a scheme to get infinitely many inaccessible cardinals if I'm not mistaken
<__marioxcc> darktenaibre: Ok. What about the HOL familiy?
<tokenrove> __marioxcc: you might want to ask about this stuff on channels more oriented around formal methods, like #coq and #isabelle
<__marioxcc> Ok.
<tokenrove> i dunno about #coq, but #isabelle is fairly active, enough that you'd probably get answers within a few hours
<__marioxcc> Thanks you.
copy_ has quit [Quit: Connection closed for inactivity]
<tokenrove> also, the book "Interactive Theorem Proving and Program Development" was highly recommended to me, so I bought a copy, but haven't had time to read it. it uses coq.
<Armael> w
<__marioxcc> Thanks you. I will take a look into it.
<__marioxcc> tokenrove.
silver has quit [Read error: Connection reset by peer]
pierpa has quit [Quit: Page closed]
sam____ has joined #ocaml
<darktenaibre> __maroxcc: I'm not familiar enough with the logics there, as far as higher-order logic is concerned, PAω is clearly below ZF; iirc throwing in kind quantification lets you reach ZF in terms of strength
<darktenaibre> I guess these are mostly curiosity questions ? Unless you are into esoteric pursuits, consistency strength of the systems is not really the main criterion I'd use to differentiate them
<__marioxcc> darktenaibre: I don't really know what axioms these provers use by deafault.
<__marioxcc> Well, yes, I'm asking for consistency only because of curiosity.
sam____ has quit [Ping timeout: 268 seconds]
<__marioxcc> But I'm interested in using proof verifiers for a real-life task, which is formalization of chemical nomenclature.
<darktenaibre> for someone like me (us?) who have been away for chemistry ever since high-school, this goal is a bit abstract^^
<__marioxcc> Well, I'm interested in chemistry and a careful reading of the IUPAC "nomenclature of organic chemistry" (blue book) made me realize that we need something more serious than this.
<__marioxcc> Becuase this one is full of errors.
<__marioxcc> Not just omissions, but blatant inconsistency.
cmk_zzz has joined #ocaml
<darktenaibre> mmmm so your goal is to have an algorithm in Coq/whatever which takes as input a labelled graph representing a molecule and output a name according to guidelines as written there (https://en.wikipedia.org/wiki/IUPAC_nomenclature_of_organic_chemistry) and certify it somehow ?
deep-book-gk_ has joined #ocaml
<__marioxcc> darktenaibre: That is a secondary goal.
<__marioxcc> First I want to define a function that takes one such graph and outputs one string, which is the preferred name of the compound.
<__marioxcc> So if X and Y are molecule graphs which are isomorph (including the extra information like element, charge, etc...), then f(X)=f(Y)
<__marioxcc> I see this as a formalization of chemical nomenclature.
<__marioxcc> Currently there is no formalization. it's written in vague and very bad written (contains many omissions and contradiction) natural language.
<__marioxcc> Only once we have a formalization can we write a program to actually compute "f".
<__marioxcc> Do you have a suggestion of where to start with? What proof verifier, et cetera?
deep-book-gk_ has left #ocaml [#ocaml]
<darktenaibre> well the property that you are saying is mostly sanity check, but ok, that's what I expected
<__marioxcc> darktenaibre: Yes, of course, but I want to remark that the current nomenclature is not "sane" at all. It could not be even called a "nomenclature" properly, but only a "vague sketch of a convention".
swalk has joined #ocaml
<__marioxcc> I have no experience with proof verifiers, except a tiny bit with metamath, so what would you suggest (I mean among Coq, Isabelle, HOL4, ...)?
<darktenaibre> yep, I imagine you have to invent specs along the way (if I'm not mistaken, some people in PL have to do this while formalizing semantics of languages like C)
<darktenaibre> I am not well-versed enough in all interactive theorem provers to offer meaningful advice beyond "don't use mizar for this"
<__marioxcc> Yes, I will attempt to follow the IUPAC text, but I will have to use my own judgement whenever it is ambiguous or contradictory.
<__marioxcc> Ok. ^.^
<darktenaibre> all of those that you cite have support for extraction, so I'm guessing they are the most convenient for the goal that you have
<__marioxcc> I see.
<__marioxcc> I will be glancing at their respective documentation until I can settle on one.
<darktenaibre> the only one I am reasonable skill with is coq
<__marioxcc> Ok. What have you used Coq for, just for curiosity?
<darktenaibre> nothing too big, I have some encounters with type-theory and curry-howard in my curriculum
<__marioxcc> Ok.
<__marioxcc> Take a look at the errata of the current specification of the IUPAC notation for organic nomenclature, it's huge: http://www.chem.qmul.ac.uk/iupac/bibliog/BBerrors.html
<__marioxcc> *IUPAC standard for organic nomenclature
<__marioxcc> I have reported some more errors.
<__marioxcc> What is remarkable here is the sheer amount of errors.
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
<__marioxcc> What is funny is that
<__marioxcc> thare is a program "ACD" that is adverstised by the vendor as a way to avoid human error by generating names of compounds given their graph, but how can it avoid errors if the specification itself is erroneous?
<__marioxcc> Absurd.
<__marioxcc> This one (it's just a presentation) -> http://bulletin.acscinf.org/PDFs/247nm44.pdf
copy_ has joined #ocaml
mengu has quit [Remote host closed the connection]
<darktenaibre> welp, I don't know the field at all, but then are they not trying to push their implementation as a spec ? in a sense, they should already be helping with disambiguation of the rules
<__marioxcc> "but then are they not trying to push their implementation as a spec ?" ← if you mean saying "the output of this program *defines* the valid nomenclature", then AFAIK, nobody is doing that.
samrat_ has joined #ocaml
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
jao has quit [Ping timeout: 255 seconds]
mfp__ has quit [Ping timeout: 260 seconds]
jao has joined #ocaml
samrat_ has quit [Ping timeout: 255 seconds]
samrat_ has joined #ocaml
enterprisey has joined #ocaml
jlam has joined #ocaml
jlam__ has quit [Ping timeout: 255 seconds]
FreeBirdLjj has joined #ocaml
__marioxcc has left #ocaml [#ocaml]
samrat_ has quit [Ping timeout: 248 seconds]
swalk has quit [Quit: swalk]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
FreeBirdLjj has joined #ocaml
maxton has joined #ocaml
sam____ has quit [Ping timeout: 255 seconds]
copy_ has quit [Quit: Connection closed for inactivity]
samrat_ has joined #ocaml
ocaml079 has joined #ocaml
ocaml079 has quit [Client Quit]
samrat_ has quit [Ping timeout: 260 seconds]
jao has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
enterprisey has quit [Read error: Connection reset by peer]
sam____ has quit [Ping timeout: 255 seconds]
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
maxton_ has joined #ocaml
maxton__ has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
michael_ has joined #ocaml
sam____ has quit [Ping timeout: 248 seconds]
samrat_ has joined #ocaml
sam____ has joined #ocaml
tennix has joined #ocaml
MercurialAlchemi has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
michael_ has quit [Remote host closed the connection]
maxton_ has quit [Read error: Connection reset by peer]
sam____ has quit [Ping timeout: 240 seconds]
michael_ has joined #ocaml
sam____ has joined #ocaml
tennix has quit [Remote host closed the connection]
sam____ has quit [Ping timeout: 255 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 268 seconds]
sam____ has joined #ocaml
dakk has quit [Ping timeout: 240 seconds]
sam____ has quit [Ping timeout: 248 seconds]
ygrek has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 248 seconds]
sam____ has joined #ocaml
ygrek has quit [Ping timeout: 248 seconds]
FreeBirdLjj has joined #ocaml
MercurialAlchemi has quit [Quit: Lost terminal]
FreeBirdLjj has quit [Ping timeout: 248 seconds]
MercurialAlchemi has joined #ocaml
ziyourenxiang has quit [Ping timeout: 268 seconds]
samrat_ has quit [Ping timeout: 240 seconds]
samrat_ has joined #ocaml
_whitelogger has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
KeyJoo has joined #ocaml
enterprisey has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 248 seconds]
enterprisey has quit [Remote host closed the connection]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 255 seconds]
sam____ has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 240 seconds]
FreeBirdLjj has joined #ocaml
peterpp has joined #ocaml
mrkgnao has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
mfp__ has joined #ocaml
peterpp has quit [Ping timeout: 240 seconds]
HoloIRCUser1 has joined #ocaml
HoloIRCUser1 is now known as HoloIRCUser18789
cranmax has joined #ocaml
FreeBirdLjj has joined #ocaml
leah2 has quit [Ping timeout: 258 seconds]
FreeBirdLjj has quit [Ping timeout: 255 seconds]
HoloIRCUser has joined #ocaml
MercurialAlchemi has joined #ocaml
HoloIRCUser18789 has quit [Ping timeout: 255 seconds]
HoloIRCUser1 has joined #ocaml
HoloIRCUser has quit [Read error: Connection reset by peer]
gallais_ has quit [Ping timeout: 240 seconds]
ziyourenxiang has joined #ocaml
leah2 has joined #ocaml
HoloIRCUser1 has quit [Remote host closed the connection]
sam____ has quit [Ping timeout: 260 seconds]
samrat_ has quit [Ping timeout: 260 seconds]
FreeBirdLjj has joined #ocaml
slash^ has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
FreeBirdLjj has joined #ocaml
_whitelogger has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 248 seconds]
silver has joined #ocaml
mrkgnao has quit [Ping timeout: 255 seconds]
mrkgnao has joined #ocaml
dhil has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
sam____ has quit [Read error: Connection reset by peer]
Hannibal_Smith has joined #ocaml
mrkgnao has quit [Ping timeout: 258 seconds]
mrkgnao has joined #ocaml
sh0t has joined #ocaml
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 260 seconds]
Hannibal_Smith has quit [Quit: Leaving]
michael_ has quit [Quit: Leaving]
fraggle_ has quit [Quit: -ENOBRAIN]
fraggle_ has joined #ocaml
FreeBirdLjj has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 260 seconds]
cranmax has quit [Quit: Connection closed for inactivity]
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 268 seconds]
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 240 seconds]
gallais has joined #ocaml
jlam has joined #ocaml
samrat_ has joined #ocaml
jlam_ has quit [Ping timeout: 248 seconds]
jlam_ has joined #ocaml
<seliopou> rgrinberg wher u at?
jlam has quit [Ping timeout: 240 seconds]
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 240 seconds]
samrat_ has quit [Read error: Connection timed out]
jlam has quit [Ping timeout: 268 seconds]
malina has joined #ocaml
<rgrinberg> Hey, Chiang Mai now.
<rgrinberg> Real dope place btw. Perfect for chilling out and taking it easy
malina has quit [Remote host closed the connection]
malina has joined #ocaml
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
fraggle-boate_ has quit [Quit: Quitte]
fraggle-boate has joined #ocaml
peterpp has joined #ocaml
malina has quit [Remote host closed the connection]
enterprisey has joined #ocaml
jlam_ has joined #ocaml
KeyJoo has quit [Ping timeout: 248 seconds]
swalk has joined #ocaml
jlam_ has quit [Read error: Connection reset by peer]
jlam_ has joined #ocaml
malina has joined #ocaml
swalk has quit [Quit: swalk]
enterprisey has quit [Remote host closed the connection]
jao has joined #ocaml
<seliopou> rgrinberg that's dope
average has quit [Ping timeout: 258 seconds]
average has joined #ocaml
jlam has joined #ocaml
peterpp_ has joined #ocaml
jlam_ has quit [Ping timeout: 255 seconds]
peterpp has quit [Ping timeout: 240 seconds]
rand__ has joined #ocaml
al-damiri has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 240 seconds]
jlam_ has quit [Read error: Connection reset by peer]
jlam has joined #ocaml
chet has joined #ocaml
<chet> Hi all, I'm an ocaml beginner, was looking at following definition: https://github.com/ocaml/ocaml/blob/trunk/stdlib/list.ml#L108 and wondering:
<chet> It does match l with, but then again value of l will be shadowed when it matches with a::l ?
malina has quit [Remote host closed the connection]
<chet> should one use different variable name like a::tl instead? reusing same name l is ok as long as original l value is no longer needed?
malina has joined #ocaml
aantron_ has joined #ocaml
<octachron> chet, rebinding the same name is indeed ok when one does not need the original value
rand__ has quit [Quit: leaving]
<chet> ah, ok, I have used scheme before, there recursion was more explicit as I knew that recursion was getting smaller as (cdr l) was being used, here it looks like right hand side expression gets evaluated in environment enriched due to pattern match.
<chet> Thanks octachron.
<octachron> chet, indeed the pattern match binds variables and those bindings can be used in the rhs of the corresponding case
<octachron> this is not so different than "let f (a,b) = a + b" where the pattern "(a,b)" bound the variable "a" and "b"
samrat_ has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 248 seconds]
chet has quit [Quit: Page closed]
malina has quit [Remote host closed the connection]
aantron_ has quit [Remote host closed the connection]
aantron_ has joined #ocaml
swalk has joined #ocaml
dakk has joined #ocaml
malina has joined #ocaml
MercurialAlchemi has joined #ocaml
copy_ has joined #ocaml
ollehar has joined #ocaml
sh0t has quit [Quit: Leaving]
peterpp__ has joined #ocaml
kakadu has joined #ocaml
peterpp_ has quit [Ping timeout: 240 seconds]
kakadu_ has joined #ocaml
kakadu has quit [Ping timeout: 248 seconds]
ocaml681 has joined #ocaml
tane has joined #ocaml
swalk has quit [Quit: swalk]
dhil has quit [Ping timeout: 255 seconds]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
MercurialAlchemi has joined #ocaml
ocaml681 has quit [Quit: Page closed]
ziyourenxiang has quit [Ping timeout: 240 seconds]
sam____ has quit [Ping timeout: 255 seconds]
aantron_ has quit [Quit: leaving]
jao has quit [Ping timeout: 260 seconds]
malina has quit [Remote host closed the connection]
malina has joined #ocaml
malina has quit [Remote host closed the connection]
mrkgnao has quit [Ping timeout: 240 seconds]
samrat_ has quit [Ping timeout: 248 seconds]
swalk has joined #ocaml
riveter has joined #ocaml
mengu has joined #ocaml
jlam has quit [Read error: Connection reset by peer]
jlam has joined #ocaml
<rixed> Is there a js_of_ocaml doc somewhere that explains the "foo##.bar" notation anywhere? I'm trying to understand how this relates to Js.gen_prop but fail.
<rixed> I'd like to stop copy and pasting code when it comes to Js ... :/
KeyJoo has joined #ocaml
malina has joined #ocaml
jao has joined #ocaml
malina has quit [Ping timeout: 240 seconds]
jlam has quit [Read error: Connection reset by peer]
jlam has joined #ocaml
sam____ has joined #ocaml
swalk has quit [Quit: swalk]
peterpp__ has quit [Ping timeout: 240 seconds]
malina has joined #ocaml
<rixed> octachron: looks like it, thanks!
malina has quit [Ping timeout: 276 seconds]
pierpa has joined #ocaml
sam____ has quit [Ping timeout: 240 seconds]
ollehar has quit [Quit: ollehar]
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 255 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
sam____ has joined #ocaml
slash^ has quit [Read error: Connection reset by peer]
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
jlam_ has quit [Ping timeout: 240 seconds]
jlam has joined #ocaml
mengu has quit [Remote host closed the connection]
dhil has joined #ocaml
cranmax has joined #ocaml
peterpp__ has joined #ocaml
infinity0 has quit [Ping timeout: 255 seconds]
infinity0_ has joined #ocaml
infinity0_ has quit [Changing host]
infinity0 has joined #ocaml
swalk has joined #ocaml
sam____ has quit [Ping timeout: 240 seconds]
dakk has quit [Quit: Leaving]
FreeBirdLjj has joined #ocaml
dakk has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 260 seconds]
<peterpp__> I'm trying to figure out why I get 'Deprecated_use_float_module' and what to do about it
<peterpp__> what exactly is deprecated here?
<octachron> peterpp__, some functions/types that you are using most probably. It is hard to tell without any context
<peterpp__> I wanted to use abs_float
<octachron> You are probably using an extended standard library with a Float module and a Float.abs function
<peterpp__> you're right!
<peterpp__> thanks
<peterpp__> the error message makes more sense to me now
sam____ has joined #ocaml
mengu has joined #ocaml
mengu has quit [Ping timeout: 268 seconds]
malina has joined #ocaml
sam____ has quit [Ping timeout: 240 seconds]
ryanartecona has joined #ocaml
swalk has quit [Quit: swalk]
enterprisey has joined #ocaml
malina has quit [Remote host closed the connection]
tane has quit [Quit: Leaving]
jlam_ has joined #ocaml
jlam has quit [Killed (hobana.freenode.net (Nickname regained by services))]
jlam_ is now known as jlam
jlam_ has joined #ocaml
mengu has joined #ocaml
swalk has joined #ocaml
ryanartecona has quit [Quit: ryanartecona]
Soni has quit [Ping timeout: 248 seconds]
swalk has quit [Quit: swalk]
FreeBirdLjj has joined #ocaml
malina has joined #ocaml
Soni has joined #ocaml
<peterpp__> how can I set up merlin so that the auto complete feature also works for the extended standard library?
FreeBirdLjj has quit [Ping timeout: 248 seconds]
hdnc2_ has quit []
deep-book-gk_ has joined #ocaml
deep-book-gk_ has left #ocaml [#ocaml]
jlam_ has quit [Ping timeout: 240 seconds]
jlam__ has joined #ocaml
average has quit [Ping timeout: 258 seconds]
average has joined #ocaml
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 240 seconds]
<tizoc> ouch, jbuilder overwrites your .merlin without asking?
kakadu_ has quit [Remote host closed the connection]
malina has quit [Remote host closed the connection]
SoniEx2 has joined #ocaml
SoniEx2 has quit [Changing host]
SoniEx2 has joined #ocaml
Soni has quit [Ping timeout: 268 seconds]
peterpp__ has quit [Ping timeout: 240 seconds]
mengu has quit [Quit: Leaving...]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
silver has quit [Read error: Connection reset by peer]
ziyourenxiang has joined #ocaml
jlam__ has joined #ocaml
jlam_ has quit [Ping timeout: 255 seconds]
pierpa has quit [Quit: Page closed]