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
dakk has quit [Remote host closed the connection]
jlam_ has quit [Ping timeout: 260 seconds]
swalk has quit [Quit: swalk]
ryanartecona has joined #ocaml
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
sh0t has quit [Remote host closed the connection]
maxton has joined #ocaml
zwild has joined #ocaml
enterprisey has joined #ocaml
zwild has quit [Remote host closed the connection]
zwild has joined #ocaml
ryanartecona has quit [Quit: ryanartecona]
cranmax has quit [Quit: Connection closed for inactivity]
swalk has joined #ocaml
TarVanimelde has joined #ocaml
copy_ has quit [Quit: Connection closed for inactivity]
ygrek has quit [Ping timeout: 260 seconds]
mfp__ has quit [Ping timeout: 255 seconds]
nullx002 has quit [Ping timeout: 260 seconds]
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
freusque has quit [Ping timeout: 255 seconds]
nullx002 has joined #ocaml
axiles has quit [Ping timeout: 255 seconds]
jbrown has quit [Remote host closed the connection]
_whitelogger has joined #ocaml
freusque has joined #ocaml
axiles has joined #ocaml
jimt_ is now known as jimt
swalk has quit [Quit: swalk]
TarVanimelde has quit [Quit: TarVanimelde]
TarVanimelde has joined #ocaml
TarVanimelde has quit [Client Quit]
TarVanimelde has joined #ocaml
TarVanimelde has quit [Client Quit]
TarVanimelde has joined #ocaml
TarVanimelde has quit [Client Quit]
TarVanimelde has joined #ocaml
TarVanimelde has quit [Client Quit]
TarVanimelde has joined #ocaml
TarVanimelde has quit [Client Quit]
malina has joined #ocaml
jao has quit [Ping timeout: 255 seconds]
swalk has joined #ocaml
enterprisey has quit [Remote host closed the connection]
TarVanimelde has joined #ocaml
samrat_ has joined #ocaml
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 240 seconds]
enterprisey has joined #ocaml
malina has quit [Ping timeout: 240 seconds]
swalk has quit [Quit: swalk]
malina has joined #ocaml
enterprisey has quit [Remote host closed the connection]
MercurialAlchemi has quit [Remote host closed the connection]
MercurialAlchemi has joined #ocaml
mali__ has joined #ocaml
mali__ has quit [Client Quit]
samrat_ has quit [Ping timeout: 268 seconds]
KeyJoo has joined #ocaml
peterpp has joined #ocaml
jimmyrcom has quit [Ping timeout: 240 seconds]
peterpp has quit [Ping timeout: 240 seconds]
andreas_ has joined #ocaml
zwild has quit [Remote host closed the connection]
zwild has joined #ocaml
ygrek has joined #ocaml
zpe has joined #ocaml
dakk has joined #ocaml
dakk_ has joined #ocaml
dakk__ has joined #ocaml
zpe_ has joined #ocaml
zpe has quit [Ping timeout: 255 seconds]
dakk_ has quit [Remote host closed the connection]
dakk has quit [Remote host closed the connection]
dakk__ has quit [Remote host closed the connection]
dakk has joined #ocaml
ygrek has quit [Ping timeout: 248 seconds]
zpe_ has quit [Remote host closed the connection]
ziyourenxiang has joined #ocaml
zwild has quit [Ping timeout: 260 seconds]
zwild has joined #ocaml
zwild has quit [Ping timeout: 240 seconds]
lostman has quit [Quit: Connection closed for inactivity]
kakadu has joined #ocaml
dhil has joined #ocaml
zwild has joined #ocaml
zwild has quit [Client Quit]
kakadu_ has joined #ocaml
kakadu has quit [Ping timeout: 258 seconds]
mfp__ has joined #ocaml
dhil has quit [Ping timeout: 240 seconds]
ziyourenxiang has quit [Ping timeout: 260 seconds]
dhil has joined #ocaml
malina has quit [Ping timeout: 255 seconds]
zaquest has quit [Quit: Leaving]
jmiven has quit [Quit: co'o]
zaquest has joined #ocaml
jmiven has joined #ocaml
malina has joined #ocaml
BitPuffin|osx has joined #ocaml
ziyourenxiang has joined #ocaml
kakadu_ has quit [Remote host closed the connection]
silver has joined #ocaml
dhil has quit [Ping timeout: 240 seconds]
troydm has quit [Ping timeout: 240 seconds]
jlam__ has joined #ocaml
jlam_ has quit [Ping timeout: 240 seconds]
grayswandyr has joined #ocaml
<grayswandyr> hi I'm looking for qtest/iteml connoiseurs. Do you know whether it is possible to "inject" some code in a module and then to refer to it in the test comments of another module? E.g. I define a generator to type M.t in module M. And then a generator for type N.t (which depends on M.t) in N.
swalk has joined #ocaml
<companion_cube> I don't think so, it's purely syntactic
<companion_cube> you should probably have some (test-only) module with the generators/printers/invariants you want to export
<grayswandyr> ok thank you
jao has joined #ocaml
dhil has joined #ocaml
jbrown has joined #ocaml
sh0t has joined #ocaml
swalk has quit [Quit: swalk]
grayswandyr has quit [Quit: Page closed]
cranmax has joined #ocaml
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 240 seconds]
jlam__ has joined #ocaml
jlam_ has quit [Ping timeout: 276 seconds]
swalk has joined #ocaml
KeyJoo has quit [Ping timeout: 246 seconds]
malina has quit [Remote host closed the connection]
samrat_ has joined #ocaml
flo2 has quit [Remote host closed the connection]
mrvn has joined #ocaml
samrat_ has quit [Ping timeout: 246 seconds]
BitPuffin|osx has quit [Ping timeout: 240 seconds]
MercurialAlchemi has quit [Remote host closed the connection]
MercurialAlchemi has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 255 seconds]
FreeBirdLjj has joined #ocaml
aciniglio has joined #ocaml
two_wheels has joined #ocaml
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 240 seconds]
jlam__ has joined #ocaml
kolko has quit [Read error: Connection reset by peer]
kolko has joined #ocaml
jlam_ has quit [Ping timeout: 240 seconds]
enterprisey has joined #ocaml
ryanartecona has joined #ocaml
kakadu has joined #ocaml
kakadu_ has joined #ocaml
kakadu has quit [Ping timeout: 260 seconds]
freusque has quit [Quit: WeeChat 1.9]
<kakadu_> Folks, does new opam 2.0 ugrade 1.2.x repositories correctly?
<kakadu_> I tried to use multicore repo but after upgrade there is no inetersting compiler in `opam switch list-available`.
dhil has quit [Ping timeout: 240 seconds]
FreeBirdLjj has quit []
maxton__ has joined #ocaml
TarVanimelde has quit [Quit: TarVanimelde]
dhil has joined #ocaml
kakadu_ is now known as kakadu
cranmax has quit [Quit: Connection closed for inactivity]
Sakarah has joined #ocaml
iZsh has quit [Ping timeout: 255 seconds]
iZsh has joined #ocaml
maxton has joined #ocaml
ryanartecona has quit [Quit: ryanartecona]
ryanartecona has joined #ocaml
sh0t has quit [Ping timeout: 248 seconds]
samrat_ has joined #ocaml
sh0t has joined #ocaml
copy_ has joined #ocaml
enterprisey has quit [Ping timeout: 255 seconds]
aciniglio has quit [Ping timeout: 240 seconds]
two_wheels has quit [Quit: Textual IRC Client: www.textualapp.com]
enterprisey has joined #ocaml
KeyJoo has joined #ocaml
TheLemonMan has joined #ocaml
maarhart_ has joined #ocaml
maarhart_ has quit [Client Quit]
dhil has quit [Ping timeout: 260 seconds]
ziyourenxiang has quit [Ping timeout: 260 seconds]
tane has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 255 seconds]
ryanartecona has quit [Quit: ryanartecona]
jlam_ has joined #ocaml
jlam_ has quit [Read error: Connection reset by peer]
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 248 seconds]
dhil has joined #ocaml
jlam__ has joined #ocaml
jlam__ has quit [Read error: Connection reset by peer]
jlam__ has joined #ocaml
jlam_ has quit [Ping timeout: 255 seconds]
peterpp has joined #ocaml
samrat_ has quit [Ping timeout: 260 seconds]
fraggle_ has quit [Quit: -ENOBRAIN]
MercurialAlchemi has joined #ocaml
ryanartecona has joined #ocaml
sam____ has joined #ocaml
pierpa has joined #ocaml
tane has quit [Quit: Leaving]
TheLemonMan has quit [Quit: "It's now safe to turn off your computer."]
ryanartecona has quit [Quit: ryanartecona]
enterprisey has quit [Remote host closed the connection]
sh0t has quit [Remote host closed the connection]
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 248 seconds]
dhil has quit [Ping timeout: 240 seconds]
infinity0_ has joined #ocaml
infinity0_ has quit [Changing host]
infinity0 is now known as Guest45409
infinity0 has joined #ocaml
Guest45409 has quit [Killed (hobana.freenode.net (Nickname regained by services))]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
sam____ has quit [Ping timeout: 260 seconds]
ryanartecona has joined #ocaml
mengu has joined #ocaml
KeyJoo has quit [Ping timeout: 248 seconds]
sam____ has joined #ocaml
fraggle_ has joined #ocaml
ryanartecona has quit [Quit: ryanartecona]
jlam__ has joined #ocaml
sam____ has quit [Ping timeout: 248 seconds]
jlam_ has quit [Ping timeout: 240 seconds]
ryanartecona has joined #ocaml
peterpp has quit [Ping timeout: 240 seconds]
mengu has quit [Remote host closed the connection]
ryanartecona has quit [Quit: ryanartecona]
mengu has joined #ocaml
jlam_ has joined #ocaml
jlam_ has quit [Read error: Connection reset by peer]
jlam_ has joined #ocaml
mengu has quit [Ping timeout: 260 seconds]
jlam__ has quit [Ping timeout: 260 seconds]
mengu has joined #ocaml
__marioxcc has joined #ocaml
<__marioxcc> Hello.
<__marioxcc> I'm trying to decide whether to learn ML or OCaml. I know that ML has a language specification. Is there any such specification for OCaml or is it defined only by the implementation (like PHP)?
<j0sh> Standard ML is formally verified, yeah. OCaml, only a subset. but i dont think that'll help much if you're trying to learn the language without any prior FP exposure
<tokenrove> __marioxcc: as far as I know there is no standard, but you might find http://caml.inria.fr/pub/docs/manual-ocaml/language.html useful
jimmyrcom has joined #ocaml
<__marioxcc> tokenrove: Ok.
<__marioxcc> Why should I learn OCaml or SML first?
<__marioxcc> (I am familiar with Common Lisp and somewhat familar with Haskell, if that is relevant)
<tokenrove> what do you want to do with the language you learn first?
<__marioxcc> tokenrove: Nothing in particular. I am interested in computerized proof verification (E.g. as in HOL4 or Coq), and I have noticed that most proof assistants/verifiers are written in OCaml or SML.
<tokenrove> (both are fine languages. SML has a variety of interesting implementations. OCaml is overall more practical and popular, but this doesn't mean practical work can't be done in SML.)
<Armael> ocaml has strictly more features than sml, and better tooling
<__marioxcc> Could you please give me an example of the "extra features" that could be useful to solve a practical problem?
<tokenrove> __marioxcc: although I haven't checked to see how up to date this is, I found this comparison useful a long time ago: http://adam.chlipala.net/mlcomp/
<__marioxcc> tokenrove: Yes, I have already read it. :)
<tokenrove> since the last time I checked that page, many syntax easements have been made in ocaml, though
<Armael> I'd say the more powerful module system (the signature language in SML is quite restricted)
<Armael> GADTs are nice too
<__marioxcc> What's GADT?
<Armael> depends on what is your notion of "solving a practical problem"
<Armael> a generalization of "sum types"
<tokenrove> from a really practical point of view, the availability of a package manager, a library ecosystem, and so on makes a big difference to quickly solving practical problems in ocaml.
<Armael> you have those in haskell as well
<Armael> also yes, on the tooling side, opam, merlin and such are great
<__marioxcc> Ok.
<__marioxcc> (17:58:18) j0sh: Standard ML is formally verified, yeah. OCaml, only a subset. but i dont think that'll help much if you're trying to learn the language without any prior FP exposure
<__marioxcc> ↑ Formaly verified? Don't you mean formally *defined*?
<j0sh> __marioxcc: you're right, i was thinking of the formal definition of SML's semantics http://sml-family.org/sml97-defn.pdf
<__marioxcc> j0sh: Ok. :)
<__marioxcc> Do you have any experience with formal proof assistants/verifiers?
Sakarah has quit [Remote host closed the connection]
<j0sh> zero :) hence why i got them mixed up.
<__marioxcc> Oh, ok.
<__marioxcc> I asked because I want to make a computer readable formalization of chemical nomenclature.
<j0sh> a few folks in this channel have that experience though. but it's the start of the weekend, and things are typically a bit slow in here then.
andreas_ has quit [Quit: Connection closed for inactivity]
<__marioxcc> I see.
<__marioxcc> Like #lisp
swalk has quit [Quit: swalk]
swalk has joined #ocaml
<Armael> __marioxcc: I have some experience with HOL4 and Coq
swalk has quit [Client Quit]
<__marioxcc> Armael: Very good. I want to formalize chemical nomenclature, given that the current standard is full of contradictions.
peterpp has joined #ocaml
<__marioxcc> But I have never used any system like this.
<__marioxcc> Well, I have used metamath, but only for "toy" theories, nothing serious.
<__marioxcc> What should be the first step? I'm reading this right now: https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
<Armael> where did you get to learn metamath?
<__marioxcc> I don't understand.
kakadu has quit [Remote host closed the connection]
<Armael> I'm juste curious how you went to know about metamath
<Armael> to me it seems like even more niche than coq or hol4
<__marioxcc> Armael: Oh, I do not remember how I heard about metamath.
<__marioxcc> But I learned about the language and the verifier itself through the book: http://us.metamath.org/downloads/metamath.pdf
<__marioxcc> And the page http://us.metamath.org/mpeuni/mmset.html , of course.
<__marioxcc> Armael: Well, probably yes. It's meant to be a minimalistic verifier where proofs are shown from the smallest logical steps, and there is minimal automation.
sam____ has joined #ocaml
<__marioxcc> So it is not very practical to "get things done".
<__marioxcc> Armael: Can you suggest how should I start learning how to use these proof assistants?
<__marioxcc> They are very different from Metamath. Nothing of what I learned for Metamath seems to carry over.
<Armael> I guess pick up some Coq tutorial/textbook?
<Armael> other people may have more precise recommendations
<__marioxcc> I was reading a tutorial, but it leaves many questions unanswered. I am currently reading this: https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
<__marioxcc> (yes, I know it's not Coq-specific)
<__marioxcc> Armael: How do HAL* and Coq compare?
<__marioxcc> (to each other)
<Armael> you mean HOL*?
<__marioxcc> Yes, I mistyped.
<__marioxcc> HOL4, Hol-light.
<__marioxcc> I don't know if there are other members of the HOL family still developed.
sam____ has quit [Ping timeout: 240 seconds]
<Armael> well I guess the main difference is the underlying theory: HOL* is higher order logic, Coq is dependently typed
kolko has quit [Ping timeout: 240 seconds]
<Armael> Coq's theory is more powerful
<__marioxcc> I don't really know what "dependently typed" means. I know what higher-order logic means (But I'm not at all knowledgeable on it).
<__marioxcc> Are any of these theorem verifiers equiconsistent with any mainstream set theory? (E.g. ZF, ZFC, ZFC+some large cardinals)?
<Armael> no, Coq is based on type theory, not on set theory
<__marioxcc> What does that mean, regarding expressive power and relative consistency?
<Armael> I don't want to say something incorrect so you might have to wait for someone more knowledgeable than me
<__marioxcc> Ok. :)
ziyourenxiang has joined #ocaml
<__marioxcc> Armael: What have you used Coq and HOL4 for?